Complex interval arithmic (on top of 64-bit fixed point intervals)

@[unbox]

structure Box : Type

Rectangular boxes of complex numbers

• re : Interval
• im : Interval

instance instDecidableEqBox : DecidableEq Box

Equations

• instDecidableEqBox = instDecidableEqBox.decEq

def instDecidableEqBox.decEq (x✝ x✝¹ : Box) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqBox.decEq { re := a, im := a_1 } { re := b, im := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance instBEqBox : BEq Box

Equations

• instBEqBox = { beq := instBEqBox.beq }

def instBEqBox.beq : Box → Box → Bool

Equations

• instBEqBox.beq { re := a, im := a_1 } { re := b, im := b_1 } = (a == b && a_1 == b_1)
• instBEqBox.beq x✝¹ x✝ = false

instance Box.instLawfulBEq : LawfulBEq Box

Box has nice equality

theorem Box.ext_iff (z w : Box) : z = w ↔ z.re = w.re ∧ z.im = w.im

Reduce Box s equality to Interval equality

instance Box.instRepr : Repr Box

Equations

• Box.instRepr = { reprPrec := fun (z : Box) (x : ℕ) => Std.Format.text "(" ++ repr z.re ++ Std.Format.text " + " ++ repr z.im ++ Std.Format.text "i⟩" }

@[simp]

theorem Box.mem_image2_iff {z : ℂ} {s t : Set ℝ} : z ∈ Set.image2 (fun (r i : ℝ) => { re := r, im := i }) s t ↔ z.re ∈ s ∧ z.im ∈ t

Simplification of ∈ image2 for Box

instance Box.instApprox : Approx Box ℂ

Box approximates ℂ

Equations

• Box.instApprox = { approx := fun (z : Box) (z' : ℂ) => approx z.re z'.re ∧ approx z.im z'.im }

instance Box.instZero : Zero Box

Box zero

Equations

• Box.instZero = { zero := { re := 0, im := 0 } }

instance Box.instOne : One Box

Box one

Equations

• Box.instOne = { one := { re := 1, im := 0 } }

instance Box.instNeg : Neg Box

Box negation

Equations

• Box.instNeg = { neg := fun (x : Box) => { re := -x.re, im := -x.im } }

instance Box.instAdd : Add Box

Box addition

Equations

• Box.instAdd = { add := fun (x y : Box) => { re := x.re + y.re, im := x.im + y.im } }

instance Box.instSub : Sub Box

Box subtraction

Equations

• Box.instSub = { sub := fun (x y : Box) => { re := x.re - y.re, im := x.im - y.im } }

instance Box.instStar : Star Box

Complex conjugation

Equations

• Box.instStar = { star := fun (x : Box) => { re := x.re, im := -x.im } }

instance Box.instMul : Mul Box

Box multiplication

Equations

• Box.instMul = { mul := fun (z w : Box) => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

instance Box.instSMulInterval : SMul Interval Box

Interval * Box

Equations

• Box.instSMulInterval = { smul := fun (x : Interval) (z : Box) => { re := x * z.re, im := x * z.im } }

def Box.sqr (z : Box) : Box

Box squaring (tighter than z * z)

Equations

• z.sqr = { re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 }

@[irreducible]

def Box.scaleB (z : Box) (t : Int64) : Box

Power of two scaling

Equations

• z.scaleB t = { re := z.re.scaleB t, im := z.im.scaleB t }

theorem Box.neg_def {z : Box} : -z = { re := -z.re, im := -z.im }

theorem Box.add_def {z w : Box} : z + w = { re := z.re + w.re, im := z.im + w.im }

theorem Box.sub_def {z w : Box} : z - w = { re := z.re - w.re, im := z.im - w.im }

theorem Box.mul_def {z w : Box} : z * w = { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re }

theorem Box.smul_def {x : Interval} {z : Box} : x • z = { re := x * z.re, im := x * z.im }

@[simp]

theorem Box.re_conj {z : Box} : (star z).re = z.re

@[simp]

theorem Box.im_conj {z : Box} : (star z).im = -z.im

@[simp]

theorem Box.re_zero : re 0 = 0

@[simp]

theorem Box.im_zero : im 0 = 0

@[simp]

theorem Box.re_one : re 1 = 1

@[simp]

theorem Box.im_one : im 1 = 0

@[simp]

theorem Box.approx_zero_iff {z' : ℂ} : approx 0 z' ↔ z' = 0

@[simp]

theorem Box.re_neg {z : Box} : (-z).re = -z.re

@[simp]

theorem Box.im_neg {z : Box} : (-z).im = -z.im

@[simp]

theorem Box.re_smul {x : Interval} {z : Box} : (x • z).re = x * z.re

@[simp]

theorem Box.im_smul {x : Interval} {z : Box} : (x • z).im = x * z.im

theorem Box.approx_re {z : ℂ} {w : Box} (zw : approx w z) : approx w.re z.re

Prove re ∈ via full ∈

theorem Box.approx_im {z : ℂ} {w : Box} (zw : approx w z) : approx w.im z.im

Prove im ∈ via full ∈

theorem Box.approx_iff_ext {z : ℂ} {w : Box} : approx w z ↔ approx w.re z.re ∧ approx w.im z.im

Split ∈ approx into components

instance Box.instApproxZeroComplex : ApproxZero Box ℂ

instance Box.instApproxZeroIffComplex : ApproxZeroIff Box ℂ

instance Box.instApproxOneComplex : ApproxOne Box ℂ

instance Box.instApproxStarComplex : ApproxStar Box ℂ

star is conservative

theorem Box.approx_conj {z : Box} {z' : ℂ} (m : approx z z') : approx (star z) ((starRingEnd ℂ) z')

instance Box.instApproxNegComplex : ApproxNeg Box ℂ

Box.neg respects approx

instance Box.instApproxAddComplex : ApproxAdd Box ℂ

Box.add respects approx

instance Box.instApproxSubComplex : ApproxSub Box ℂ

Box.sub respects approx

noncomputable instance Box.instApproxAddGroupComplex : ApproxAddGroup Box ℂ

Box approximates ℂ as an additive group

Equations

• One or more equations did not get rendered due to their size.

instance Box.instApproxMulComplex : ApproxMul Box ℂ

Box multiplication approximates ℂ

theorem Box.approx_smul {z : Box} {z' : ℂ} {x : Interval} {x' : ℝ} (ax : approx x x') (az : approx z z') : approx (x • z) (x' • z')

Interval • Box approximates ℂ

noncomputable instance Box.instApproxRingComplex : ApproxRing Box ℂ

Box approximates ℂ as a ring

Equations

• One or more equations did not get rendered due to their size.

theorem Box.approx_sqr {z : Box} {z' : ℂ} (az : approx z z') : approx z.sqr (z' ^ 2)

Box squaring approximates ℂ

theorem Box.approx_scaleB {z : Box} {z' : ℂ} (az : approx z z') (t : Int64) : approx (z.scaleB t) (z' * 2 ^ ↑t)

Box scaling approximates ℂ

theorem Box.approx_scaleB_one {z : Box} {z' : ℂ} (az : approx z z') : approx (z.scaleB 1) (2 * z')

Box doubling approximates ℂ

Multiplication and division by I

@[irreducible]

def Box.mul_I (z : Box) : Box

Equations

• z.mul_I = { re := -z.im, im := z.re }

@[irreducible]

def Box.div_I (z : Box) : Box

Equations

• z.div_I = { re := z.im, im := -z.re }

theorem Box.approx_mul_I {z : Box} {z' : ℂ} (m : approx z z') : approx z.mul_I (z' * Complex.I)

theorem Box.approx_div_I {z : Box} {z' : ℂ} (m : approx z z') : approx z.div_I (z' / Complex.I)

theorem Box.approx_div_I' {z : Box} {z' : ℂ} (m : approx z z') : approx z.div_I (-z' * Complex.I)

@[simp]

theorem Box.div_I_mul_I {z : Box} : z.div_I.mul_I = z

@[simp]

theorem Box.mul_I_div_I {z : Box} : z.mul_I.div_I = z

Square magnitude

@[irreducible]

def Box.normSq (z : Box) : Interval

Box square magnitude

Equations

• z.normSq = z.re.sqr + z.im.sqr

theorem Box.approx_normSq {z : Box} {z' : ℂ} (m : approx z z') : approx z.normSq (‖z'‖ ^ 2)

normSq is conservative

theorem Box.approx_normSq' {z : Box} {z' : ℂ} (m : approx z z') : approx z.normSq (Complex.normSq z')

normSq is conservative

theorem Box.sqrt_normSq_le_abs {z : Box} {z' : ℂ} (m : approx z z') : √z.normSq.lo.val ≤ ‖z'‖

Lower bounds on normSq produce lower bounds on contained radii

theorem Box.abs_le_sqrt_normSq {z : Box} {z' : ℂ} (m : approx z z') (n : z.normSq ≠ nan) : ‖z'‖ ≤ √z.normSq.hi.val

Upper bounds on normSq produce upper bounds on contained radii

Conversion

@[irreducible]

def Complex.ofRat (z : ℚ × ℚ) : ℂ

Equations

• ↑z = { re := ↑z.1, im := ↑z.2 }

theorem Complex.ofRat_def (z : ℚ × ℚ) : ↑z = { re := ↑z.1, im := ↑z.2 }

noncomputable instance Box.instCoeProdRatComplex : Coe (ℚ × ℚ) ℂ

Equations

• Box.instCoeProdRatComplex = { coe := fun (z : ℚ × ℚ) => ↑z }

@[irreducible]

def Box.ofRat (z : ℚ × ℚ) : Box

Equations

• Box.ofRat z = { re := ↑z.1, im := ↑z.2 }

theorem Box.approx_ofRat (z : ℚ × ℚ) : approx (ofRat z) ↑z

Unbundled instances

instance Box.instNegZeroClass' : NegZeroClass' Box

instance Box.instAddZeroClass' : AddZeroClass' Box

instance Box.instSubZeroClassInterval : SubZeroClass Interval