Interval approximations for complex numbers

IsComputableℂ x packages IsComputable approximations for the real and imaginary parts of a complex number x, and is closed under the field operations, powers, conjugation, norm and inner product. This also provides DecidableEq and (with ComplexOrder) Decidable comparison instances; like their real counterparts, these comparison instances are classical and noncomputable.

class IsComputableℂ (x : ℂ) : Type

Type class stating that x : ℂ has a ComputableℝSeq for its real and imaginary parts. Note that we can't define this as IsComputable x.re + IsComputable x.im, because then (if x is a noncomputable expression) this will be a noncomputable expression.

• re : IsComputable x.re

  An interval-approximation witness for the real part.

• im : IsComputable x.im

  An interval-approximation witness for the imaginary part.

@[reducible]

def IsComputableℂ.liftEq {x y : ℂ} (h : x = y) [hx : IsComputableℂ x] : IsComputableℂ y

Turns one IsComputableℂ into another one, given a proof that they're equal. This is directly analogous to decidable_of_iff, as a way to avoid Eq.rec on data-carrying instances.

Equations

• IsComputableℂ.liftEq h = { re := IsComputable.liftEq ⋯ IsComputableℂ.re, im := IsComputable.liftEq ⋯ IsComputableℂ.im }

@[implicit_reducible]

instance IsComputableℂ.instComputableRe (x : ℂ) [hx : IsComputableℂ x] : IsComputable x.re

Equations

• IsComputableℂ.instComputableRe x = IsComputableℂ.re

@[implicit_reducible]

instance IsComputableℂ.instComputableIm (x : ℂ) [hx : IsComputableℂ x] : IsComputable x.im

Equations

• IsComputableℂ.instComputableIm x = IsComputableℂ.im

@[implicit_reducible]

instance IsComputableℂ.instComputableRI (r : ℝ) [hr : IsComputable r] {i : ℝ} [hi : IsComputable i] : IsComputableℂ { re := r, im := i }

Equations

• IsComputableℂ.instComputableRI r = { re := hr, im := hi }

@[implicit_reducible]

instance IsComputableℂ.instComputableI : IsComputableℂ Complex.I

Equations

• IsComputableℂ.instComputableI = { re := { seq := 0, prop := IsComputableℂ.instComputableI._proof_1 }, im := { seq := 1, prop := IsComputableℂ.instComputableI._proof_2 } }

@[implicit_reducible]

instance IsComputableℂ.instComputableNat (n : ℕ) : IsComputableℂ ↑n

Equations

• IsComputableℂ.instComputableNat n = { re := { seq := ComputableℝSeq.ofRat ↑n, prop := ⋯ }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableInt (z : ℤ) : IsComputableℂ ↑z

Equations

• IsComputableℂ.instComputableInt z = { re := { seq := ComputableℝSeq.ofRat ↑z, prop := ⋯ }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableRat (q : ℚ) : IsComputableℂ ↑q

Equations

• IsComputableℂ.instComputableRat q = { re := { seq := ComputableℝSeq.ofRat q, prop := ⋯ }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableReal (r : ℝ) [hr : IsComputable r] : IsComputableℂ ↑r

Equations

• IsComputableℂ.instComputableReal r = { re := hr, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableOfNat0 : IsComputableℂ (OfNat.ofNat 0)

Equations

• IsComputableℂ.instComputableOfNat0 = { re := { seq := 0, prop := ComputableℝSeq.val_zero }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableOfNat1 : IsComputableℂ (OfNat.ofNat 1)

Equations

• IsComputableℂ.instComputableOfNat1 = { re := { seq := 1, prop := ComputableℝSeq.val_one }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableOfNatAtLeastTwo (n : ℕ) [n.AtLeastTwo] : IsComputableℂ (OfNat.ofNat n)

Equations

• IsComputableℂ.instComputableOfNatAtLeastTwo n = { re := { seq := ComputableℝSeq.ofRat ↑n, prop := ⋯ }, im := { seq := 0, prop := ComputableℝSeq.val_zero } }

@[implicit_reducible]

instance IsComputableℂ.instComputableNeg (x : ℂ) [hx : IsComputableℂ x] : IsComputableℂ (-x)

Equations

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

@[implicit_reducible]

instance IsComputableℂ.instComputableAdd (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : IsComputableℂ (x + y)

Equations

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

@[implicit_reducible]

instance IsComputableℂ.instComputableSub (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : IsComputableℂ (x - y)

Equations

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

@[implicit_reducible, inline]

instance IsComputableℂ.instComputableMul (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : IsComputableℂ (x * y)

Equations

• IsComputableℂ.instComputableMul x y = { re := IsComputable.liftEq ⋯ inferInstance, im := IsComputable.liftEq ⋯ inferInstance }

@[implicit_reducible]

instance IsComputableℂ.instComputableNatPow (x : ℂ) [hx : IsComputableℂ x] (n : ℕ) : IsComputableℂ (x ^ n)

Equations

• IsComputableℂ.instComputableNatPow x n = Nat.recAux (⋯.mpr inferInstance) (fun (n : ℕ) (a : IsComputableℂ (x ^ n)) => ⋯.mpr inferInstance) n

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableNormSq (x : ℂ) [hx : IsComputableℂ x] : IsComputable (Complex.normSq x)

Equations

• IsComputableℂ.instComputableNormSq x = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

instance IsComputableℂ.instComputableStar (x : ℂ) [hx : IsComputableℂ x] : IsComputableℂ ((starRingEnd ℂ) x)

Equations

• IsComputableℂ.instComputableStar x = { re := IsComputableℂ.re, im := have x_1 := IsComputableℂ.im; { seq := (fun (x : ComputableℝSeq) => -x) (IsComputable.seq x.im), prop := ⋯ } }

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableInv (x : ℂ) [hx : IsComputableℂ x] : IsComputableℂ x⁻¹

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableDiv (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : IsComputableℂ (x / y)

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableZPow (x : ℂ) [hx : IsComputableℂ x] (z : ℤ) : IsComputableℂ (x ^ z)

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableNSMul (x : ℂ) [hx : IsComputableℂ x] (n : ℕ) : IsComputableℂ (n • x)

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableZSMul (x : ℂ) [hx : IsComputableℂ x] (z : ℤ) : IsComputableℂ (z • x)

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableQSMul (x : ℂ) [hx : IsComputableℂ x] (q : ℚ) : IsComputableℂ (q • x)

Equations

• IsComputableℂ.instComputableQSMul x q = IsComputableℂ.liftEq ⋯

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableInner (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : IsComputable (inner ℝ x y)

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableNorm (x : ℂ) [hx : IsComputableℂ x] : IsComputable ‖x‖

Equations

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

@[implicit_reducible]

noncomputable instance IsComputableℂ.instComputableNNNorm (x : ℂ) [hx : IsComputableℂ x] : IsComputable ↑‖x‖₊

Equations

• IsComputableℂ.instComputableNNNorm x = IsComputableℂ.instComputableNorm x

@[implicit_reducible]

noncomputable instance IsComputableℂ.instDecidableEq (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : Decidable (x = y)

Equations

• IsComputableℂ.instDecidableEq x y = decidable_of_decidable_of_iff ⋯

@[implicit_reducible]

noncomputable instance IsComputableℂ.instDecidableLE (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : Decidable (x ≤ y)

Equations

• IsComputableℂ.instDecidableLE x y = instDecidableAnd

@[implicit_reducible]

noncomputable instance IsComputableℂ.instDecidableLT (x y : ℂ) [hx : IsComputableℂ x] [hy : IsComputableℂ y] : Decidable (x < y)

Equations

• IsComputableℂ.instDecidableLT x y = instDecidableAnd