Approximate arithmetic typeclasses

class Approx (A R : Type) : Type

A approximates R, in that we know which Rs an A corresponds to.

• approx (x : A) (y : R) : Prop

class ApproxZero (A R : Type) [Zero R] [Zero A] [Approx A R] : Prop

0 : A is conservative, and 0 only approximates 0

• approx_zero : approx 0 0

class ApproxZeroIff (A R : Type) [Zero R] [Zero A] [Approx A R] : Prop

0 : A only approximates 0

• approx_zero_imp (x : R) : approx 0 x → x = 0

class ApproxOne (A R : Type) [One R] [One A] [Approx A R] : Prop

1 : A is conservative

• approx_one : approx 1 1

class ApproxNeg (A R : Type) [Neg R] [Neg A] [Approx A R] : Prop

-A is conservative

• approx_neg {x : A} {y : R} (m : approx x y) : approx (-x) (-y)

class ApproxAdd (A R : Type) [Add R] [Add A] [Approx A R] : Prop

A + A is conservative

• approx_add {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x + y) (z + w)

class ApproxSub (A R : Type) [Sub R] [Sub A] [Approx A R] : Prop

A - A is conservative

• approx_sub {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x - y) (z - w)

class ApproxMul (A R : Type) [Mul R] [Mul A] [Approx A R] : Prop

A * A is conservative

• approx_mul {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x * y) (z * w)

class ApproxInv (A R : Type) [Inv R] [Inv A] [Approx A R] : Prop

A⁻¹ is conservative

• approx_inv {x : A} {y : R} (m : approx x y) : approx x⁻¹ y⁻¹

class ApproxStar (A R : Type) [Star R] [Star A] [Approx A R] : Prop

star A is conservative

• approx_star {x : A} {y : R} (m : approx x y) : approx (star x) (star y)

class ApproxDiv (A R : Type) [Div R] [Div A] [Approx A R] : Prop

A / A is conservative

• approx_div {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x / y) (z / w)

class ApproxSMul (A B A' B' : Type) [SMul A B] [SMul A' B'] [Approx A A'] [Approx B B'] : Prop

A • B is conservative

• approx_smul {s' : A'} {x' : B'} {s : A} {x : B} (sm : approx s s') (xm : approx x x') : approx (s • x) (s' • x')

class ApproxNatCast (A R : Type) [NatCast R] [NatCast A] [Approx A R] : Prop

A has conservative ℕ conversion

• approx_natCast {n : ℕ} : approx ↑n ↑n

class ApproxIntCast (A R : Type) [IntCast R] [IntCast A] [Approx A R] : Prop

A has conservative ℤ conversion

• approx_intCast {n : ℤ} : approx ↑n ↑n

class ApproxRatCast (A R : Type) [RatCast R] [RatCast A] [Approx A R] : Prop

A has conservative ℚ conversion

• approx_ratCast {x : ℚ} : approx ↑x ↑x

class ApproxAddGroup (A R : Type) [AddGroup R] extends Zero A, Neg A, Add A, Sub A, Approx A R, ApproxZero A R, ApproxNeg A R, ApproxAdd A R, ApproxSub A R : Type

A approximates the additive group R

• zero : A
• neg : A → A
• add : A → A → A
• sub : A → A → A
• approx (x : A) (y : R) : Prop
• approx_zero : approx 0 0
• approx_neg {x : A} {y : R} (m : approx x y) : approx (-x) (-y)
• approx_add {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x + y) (z + w)
• approx_sub {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x - y) (z - w)

class ApproxRing (A R : Type) [Ring R] extends ApproxAddGroup A R, One A, Mul A, ApproxOne A R, ApproxMul A R : Type

A approximates the ring R

• zero : A
• neg : A → A
• add : A → A → A
• sub : A → A → A
• approx (x : A) (y : R) : Prop
• approx_zero : approx 0 0
• approx_neg {x : A} {y : R} (m : approx x y) : approx (-x) (-y)
• approx_add {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x + y) (z + w)
• approx_sub {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x - y) (z - w)
• one : A
• mul : A → A → A
• approx_one : approx 1 1
• approx_mul {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x * y) (z * w)

class ApproxField (A R : Type) [Field R] extends ApproxRing A R, Div A, ApproxDiv A R : Type

A approximates the field R

• zero : A
• neg : A → A
• add : A → A → A
• sub : A → A → A
• approx (x : A) (y : R) : Prop
• approx_zero : approx 0 0
• approx_neg {x : A} {y : R} (m : approx x y) : approx (-x) (-y)
• approx_add {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x + y) (z + w)
• approx_sub {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x - y) (z - w)
• one : A
• mul : A → A → A
• approx_one : approx 1 1
• approx_mul {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x * y) (z * w)
• div : A → A → A
• approx_div {x y : A} {z w : R} (xz : approx x z) (yw : approx y w) : approx (x / y) (z / w)

theorem approx_zero_iff {R A : Type} [Approx A R] [Zero A] [Zero R] [ApproxZero A R] [ApproxZeroIff A R] (x : R) : approx 0 x ↔ x = 0

Everything approximates itself

instance instApprox {R : Type} : Approx R R

Equations

• instApprox = { approx := fun (x y : R) => x = y }

instance instApproxZero {R : Type} [Zero R] : ApproxZero R R

instance instApproxZeroIff {R : Type} [Zero R] : ApproxZeroIff R R

instance instApproxOne {R : Type} [One R] : ApproxOne R R

instance instApproxNeg {R : Type} [Neg R] : ApproxNeg R R

instance instApproxAdd {R : Type} [Add R] : ApproxAdd R R

instance instApproxSub {R : Type} [Sub R] : ApproxSub R R

instance instApproxMul {R : Type} [Mul R] : ApproxMul R R

instance instApproxInv {R : Type} [Inv R] : ApproxInv R R

instance instApproxDiv {R : Type} [Div R] : ApproxDiv R R

instance instApproxSMul {A B : Type} [SMul A B] : ApproxSMul A B A B

instance instApproxNatCast {A : Type} [NatCast A] : ApproxNatCast A A

instance instApproxIntCast {A : Type} [IntCast A] : ApproxIntCast A A

instance instApproxRatCast {A : Type} [RatCast A] : ApproxRatCast A A

Typeclass for nan

def approxSet {R A : Type} [Approx A R] (x : A) : Set R

The set of approximated elements. Default to using approx as a membership function.

Equations

• approxSet x = {y : R | approx x y}

Typeclass for nan

class Nan (A : Type) : Type

• nan : A

class ApproxNan (A R : Type) [Approx A R] [Nan A] : Prop

• approx_nan (x : R) : approx nan x

Rounding utilities

For when we approximately round up or down.

def Rounds {R A : Type} [Approx A R] [LE R] (x : A) (y : R) (up : Bool) : Prop

Equations

• Rounds x y up = ∃ (a : R), approx x a ∧ if up = true then y ≤ a else a ≤ y

@[simp]

theorem rounds_same {I : Type} [LinearOrder I] {up : Bool} {x y : I} : Rounds x y up ↔ if up = true then y ≤ x else x ≤ y

@[simp]

theorem rounds_nan {A I : Type} [LinearOrder I] {up : Bool} [Approx A I] [Nan A] [ApproxNan A I] {y : I} : Rounds nan y up

theorem rounds_neg {A I : Type} [LinearOrder I] {up : Bool} [Approx A I] [Neg A] [AddGroup I] [ApproxNeg A I] [AddLeftMono I] [AddRightMono I] {x : A} {y : I} (a : Rounds x (-y) !up) : Rounds (-x) y up

theorem Rounds.neg {A I : Type} [LinearOrder I] {up : Bool} [Approx A I] [Neg A] [AddGroup I] [ApproxNeg A I] [AddLeftMono I] [AddRightMono I] {x : A} {y : I} (a : Rounds x y !up) : Rounds (-x) (-y) up

approx machinery

Convexity of approx

class ApproxConnected (A R : Type) [Approx A R] [Preorder R] : Prop

A has a convex approx

• connected (x : A) : (approxSet x).OrdConnected

theorem approx_of_mem_Icc {R A : Type} [Approx A R] [Preorder R] [ApproxConnected A R] {a b c : R} {x : A} (xa : approx x a) (xc : approx x c) (abc : b ∈ Set.Icc a c) : approx x b

Icc ⊆ approx if the endpoints are included