Interval-Cauchy real sequences

A ComputableℝSeq carries a sequence of rational intervals (ℚInterval) that converge to a single real number, with proofs that the lower and upper rational bounds are valid and Cauchy-equivalent. This file develops the basic interval arithmetic on ℚInterval and the algebraic operations (addition, negation, multiplication, inversion) on ComputableℝSeq, culminating in a commutative semiring structure.

The interval sequence is an arbitrary function ℕ → ℚInterval, with no recursiveness requirement, so membership in this type is not computability in the computable-analysis sense. Addition, negation, and multiplication are executable interval arithmetic, while sign (and hence inversion and division, which need a nonzero witness) is defined classically and is noncomputable.

def QInterval.termℚInterval : Lean.ParserDescr

Notation ℚInterval for a nonempty rational interval.

Equations

• QInterval.termℚInterval = Lean.ParserDescr.node `QInterval.termℚInterval 1024 (Lean.ParserDescr.symbol "ℚInterval")

@[implicit_reducible]

def QInterval.instMemℝℚInterval : Membership ℝ (NonemptyInterval ℚ)

A real lies in a ℚInterval when it is between the lower and upper bounds.

Equations

• QInterval.instMemℝℚInterval = { mem := fun (s : NonemptyInterval ℚ) (a : ℝ) => ↑s.toProd.1 ≤ a ∧ a ≤ ↑s.toProd.2 }

def QInterval.mulPair (x y : NonemptyInterval ℚ) : NonemptyInterval ℚ

Multiplication on intervals of ℚ. TODO: Should generalize to any LinearOrderedField...

Equations

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

def QInterval.mulQ (x : NonemptyInterval ℚ) (y : ℚ) : NonemptyInterval ℚ

Multiplication of intervals by a ℚ. TODO: Should generalize to any LinearOrderedField

Equations

• QInterval.mulQ x y = if h : y ≥ 0 then { fst := x.toProd.1 * y, snd := x.toProd.2 * y, fst_le_snd := ⋯ } else { fst := x.toProd.2 * y, snd := x.toProd.1 * y, fst_le_snd := ⋯ }

@[implicit_reducible]

def QInterval.instMulQInterval : Mul (NonemptyInterval ℚ)

Interval multiplication on ℚInterval.

Equations

• QInterval.instMulQInterval = { mul := QInterval.mulPair }

@[implicit_reducible]

def QInterval.instHMulQIntervalQ : HMul (NonemptyInterval ℚ) ℚ (NonemptyInterval ℚ)

Multiplication of a ℚInterval by a rational scalar.

Equations

• QInterval.instHMulQIntervalQ = { hMul := QInterval.mulQ }

@[implicit_reducible]

def QInterval.instHDivQIntervalQ : HDiv (NonemptyInterval ℚ) ℚ (NonemptyInterval ℚ)

Division of a ℚInterval by a rational scalar.

Equations

• QInterval.instHDivQIntervalQ = { hDiv := fun (x : NonemptyInterval ℚ) (y : ℚ) => x * y⁻¹ }

theorem QInterval.mulPair_lb_is_lb {x y : NonemptyInterval ℚ} (xv : ℝ) : xv ∈ x → ∀ yv ∈ y, ↑(mulPair x y).toProd.1 ≤ xv * yv

theorem QInterval.mulPair_ub_is_ub {x y : NonemptyInterval ℚ} (xv : ℝ) : xv ∈ x → ∀ yv ∈ y, ↑(mulPair x y).toProd.2 ≥ xv * yv

theorem QInterval.mem_mulPair {x y : NonemptyInterval ℚ} (xv : ℝ) : xv ∈ x → ∀ yv ∈ y, xv * yv ∈ mulPair x y

@[implicit_reducible]

def QInterval.instRatCastQInterval : RatCast (NonemptyInterval ℚ)

The constant interval at a rational number.

Equations

• QInterval.instRatCastQInterval = { ratCast := fun (q : ℚ) => NonemptyInterval.pure q }

@[implicit_reducible]

def QInterval.instOfNatQInterval {n : ℕ} : OfNat (NonemptyInterval ℚ) n

The constant interval at a numeric literal.

Equations

• QInterval.instOfNatQInterval = { ofNat := NonemptyInterval.pure ↑n }

structure ComputableℝSeq : Type

Structure for sequences that converge to some real number from above and below. lub is a function that gives upper and lower bounds, bundled so it can reuse computation; it is an arbitrary function ℕ → ℚInterval, with no recursiveness requirement. hcl and hcu assert that the two bounds are Cauchy sequences, hlub asserts that they're valid lower and upper bounds, and heq' asserts that they converge to a common value. Use ComputableℝSeq.mk to construct with regards to a reference real value.

The defs lb, ub are the actual CauSeq's , val is the associated real number, and hlb, hub, and heq relate lb ub and val to each other.

• mk' :: (
• lub : ℕ → NonemptyInterval ℚ

  The bundled lower and upper rational bounds at each step n.

• hcl : IsCauSeq abs fun (n : ℕ) => (self.lub n).toProd.1
• hcu : IsCauSeq abs fun (n : ℕ) => (self.lub n).toProd.2
• hlub (n : ℕ) : ↑(self.lub n).toProd.1 ≤ Real.mk ⟨fun (n : ℕ) => (self.lub n).toProd.1, ⋯⟩ ∧ ↑(self.lub n).toProd.2 ≥ Real.mk ⟨fun (n : ℕ) => (self.lub n).toProd.1, ⋯⟩
• heq' : let lb := ⟨fun (n : ℕ) => (self.lub n).toProd.1, ⋯⟩; let ub := ⟨fun (n : ℕ) => (self.lub n).toProd.2, ⋯⟩; lb ≈ ub
• )

def ComputableℝSeq.lb (x : ComputableℝSeq) : CauSeq ℚ abs

The lower-bound Cauchy sequence of a ComputableℝSeq.

Equations

• x.lb = ⟨fun (n : ℕ) => (x.lub n).toProd.1, ⋯⟩

def ComputableℝSeq.ub (x : ComputableℝSeq) : CauSeq ℚ abs

The upper-bound Cauchy sequence of a ComputableℝSeq.

Equations

• x.ub = ⟨fun (n : ℕ) => (x.lub n).toProd.2, ⋯⟩

@[irreducible]

def ComputableℝSeq.val (x : ComputableℝSeq) : ℝ

Get the real value determined by the sequence. (Irreducibly) given here as the limit of the lower bound sequence.

Equations

• x.val = Real.mk x.lb

theorem ComputableℝSeq.val_def (x : ComputableℝSeq) : x.val = Real.mk x.lb

theorem ComputableℝSeq.heq (x : ComputableℝSeq) : x.lb ≈ x.ub

theorem ComputableℝSeq.lb_eq_ub (x : ComputableℝSeq) : Real.mk x.lb = Real.mk x.ub

theorem ComputableℝSeq.val_eq_mk_lb (x : ComputableℝSeq) : x.val = Real.mk x.lb

theorem ComputableℝSeq.val_eq_mk_ub (x : ComputableℝSeq) : x.val = Real.mk x.ub

theorem ComputableℝSeq.hlb (x : ComputableℝSeq) (n : ℕ) : ↑(↑x.lb n) ≤ x.val

theorem ComputableℝSeq.hub (x : ComputableℝSeq) (n : ℕ) : ↑(↑x.ub n) ≥ x.val

theorem ComputableℝSeq.val_mem_interval (x : ComputableℝSeq) (n : ℕ) : x.val ∈ x.lub n

theorem ComputableℝSeq.val_uniq {x : ℝ} {s : ComputableℝSeq} (hlb : ∀ (n : ℕ), ↑(↑s.lb n) ≤ x) (hub : ∀ (n : ℕ), ↑(↑s.ub n) ≥ x) : s.val = x

If a real number x is bounded below and above by a sequence, it must be the value of that sequence.

def ComputableℝSeq.mk (x : ℝ) (lub : ℕ → NonemptyInterval ℚ) (hcl : IsCauSeq abs fun (n : ℕ) => (lub n).toProd.1) (hcu : IsCauSeq abs fun (n : ℕ) => (lub n).toProd.2) (hlb : ∀ (n : ℕ), ↑(lub n).toProd.1 ≤ x) (hub : ∀ (n : ℕ), ↑(lub n).toProd.2 ≥ x) (heq : have lb := ⟨fun (n : ℕ) => (lub n).toProd.1, hcl⟩; have ub := ⟨fun (n : ℕ) => (lub n).toProd.2, hcu⟩; lb ≈ ub) : ComputableℝSeq

Make a computable sequence for x from a separate lower and upper bound CauSeq.

Equations

• ComputableℝSeq.mk x lub hcl hcu hlb hub heq = { lub := lub, hcl := hcl, hcu := hcu, hlub := ⋯, heq' := heq }

theorem ComputableℝSeq.mk_val_eq_val {x : ℝ} {v : ℕ → NonemptyInterval ℚ} {h₁ : IsCauSeq abs fun (n : ℕ) => (v n).toProd.1} {h₂ : IsCauSeq abs fun (n : ℕ) => (v n).toProd.2} {h₃ : ∀ (n : ℕ), ↑(v n).toProd.1 ≤ x} {h₄ : ∀ (n : ℕ), ↑(v n).toProd.2 ≥ x} {h₅ : have lb := ⟨fun (n : ℕ) => (v n).toProd.1, h₁⟩; have ub := ⟨fun (n : ℕ) => (v n).toProd.2, h₂⟩; lb ≈ ub} : (mk x v h₁ h₂ h₃ h₄ h₅).val = x

theorem ComputableℝSeq.lb_le_ub (x : ComputableℝSeq) (n : ℕ) : ↑x.lb n ≤ ↑x.ub n

theorem ComputableℝSeq.ext {x y : ComputableℝSeq} (h₁ : ∀ (n : ℕ), ↑x.lb n = ↑y.lb n) (h₂ : ∀ (n : ℕ), ↑x.ub n = ↑y.ub n) : x = y

theorem ComputableℝSeq.ext_iff {x y : ComputableℝSeq} : x = y ↔ (∀ (n : ℕ), ↑x.lb n = ↑y.lb n) ∧ ∀ (n : ℕ), ↑x.ub n = ↑y.ub n

def ComputableℝSeq.ofRat (q : ℚ) : ComputableℝSeq

All rational numbers q have a computable sequence: the constant sequence q.

Equations

• ComputableℝSeq.ofRat q = ComputableℝSeq.mk (↑q) (fun (x : ℕ) => NonemptyInterval.pure q) ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance ComputableℝSeq.natCast : NatCast ComputableℝSeq

Equations

• ComputableℝSeq.natCast = { natCast := fun (n : ℕ) => ComputableℝSeq.ofRat ↑n }

@[implicit_reducible]

instance ComputableℝSeq.intCast : IntCast ComputableℝSeq

Equations

• ComputableℝSeq.intCast = { intCast := fun (z : ℤ) => ComputableℝSeq.ofRat ↑z }

@[implicit_reducible]

instance ComputableℝSeq.ratCast : RatCast ComputableℝSeq

Equations

• ComputableℝSeq.ratCast = { ratCast := fun (q : ℚ) => ComputableℝSeq.ofRat q }

def ComputableℝSeq.add (x y : ComputableℝSeq) : ComputableℝSeq

Addition of computable real sequences.

Equations

• x.add y = ComputableℝSeq.mk (x.val + y.val) (fun (n : ℕ) => x.lub n + y.lub n) ⋯ ⋯ ⋯ ⋯ ⋯

def ComputableℝSeq.neg (x : ComputableℝSeq) : ComputableℝSeq

Negation of a computable real sequence.

Equations

• x.neg = ComputableℝSeq.mk (-x.val) (fun (n : ℕ) => -x.lub n) ⋯ ⋯ ⋯ ⋯ ⋯

def ComputableℝSeq.sub (x y : ComputableℝSeq) : ComputableℝSeq

Subtraction of computable real sequences.

Equations

• x.sub y = x.add y.neg

def ComputableℝSeq.mul' (x y : ComputableℝSeq) : ℕ → NonemptyInterval ℚ

"Bundled" multiplication to give lower and upper bounds. This bundling avoids the need to call lb and ub separately for each half (which, in a large product, leads to an exponential slowdown). This could be further optimized to use only two ℚ multiplications instead of four, when the sign is apparent.

Equations

• x.mul' y n = QInterval.mulPair (x.lub n) (y.lub n)

def ComputableℝSeq.mulLb (x y : ComputableℝSeq) : CauSeq ℚ abs

More friendly expression for the lower bound for multiplication, as a CauSeq.

Equations

• x.mulLb y = x.lb * y.lb ⊓ x.ub * y.lb ⊓ (x.lb * y.ub ⊓ x.ub * y.ub)

def ComputableℝSeq.mulUb (x y : ComputableℝSeq) : CauSeq ℚ abs

More friendly expression for the lower bound for multiplication, as a CauSeq.

Equations

• x.mulUb y = x.lb * y.lb ⊔ x.ub * y.lb ⊔ (x.lb * y.ub ⊔ x.ub * y.ub)

theorem ComputableℝSeq.fst_mul'_eq_mulLb {x y : ComputableℝSeq} : (fun (i : NonemptyInterval ℚ) => i.toProd.1) ∘ x.mul' y = ↑(x.mulLb y)

The lower bounds from mul' are precisely the same sequence as mulLb.

theorem ComputableℝSeq.snd_mul'_eq_mulUb {x y : ComputableℝSeq} : (fun (i : NonemptyInterval ℚ) => i.toProd.2) ∘ x.mul' y = ↑(x.mulUb y)

The upper bounds from mul' are precisely the same sequence as mulUb.

theorem ComputableℝSeq.mul'_fst_iscau {x y : ComputableℝSeq} : IsCauSeq abs ((fun (i : NonemptyInterval ℚ) => i.toProd.1) ∘ x.mul' y)

The lower bounds from mul' form a Cauchy sequence.

theorem ComputableℝSeq.mul'_snd_iscau {x y : ComputableℝSeq} : IsCauSeq abs ((fun (i : NonemptyInterval ℚ) => i.toProd.2) ∘ x.mul' y)

The upper bounds from mul' form a Cauchy sequence.

theorem ComputableℝSeq.lb_ub_mul_equiv (x y : ComputableℝSeq) : x.mulLb y ≈ x.mulUb y

theorem ComputableℝSeq.mulLb_is_lb (x y : ComputableℝSeq) (n : ℕ) : ↑(↑(x.mulLb y) n) ≤ x.val * y.val

theorem ComputableℝSeq.mulUb_is_ub (x y : ComputableℝSeq) (n : ℕ) : ↑(↑(x.mulUb y) n) ≥ x.val * y.val

def ComputableℝSeq.mul (x y : ComputableℝSeq) : ComputableℝSeq

Multiplication of computable real sequences.

Equations

• x.mul y = { lub := x.mul' y, hcl := ⋯, hcu := ⋯, hlub := ⋯, heq' := ⋯ }

@[implicit_reducible]

instance ComputableℝSeq.instComputableZero : Zero ComputableℝSeq

Equations

• ComputableℝSeq.instComputableZero = { zero := ↑0 }

@[implicit_reducible]

instance ComputableℝSeq.instComputableOne : One ComputableℝSeq

Equations

• ComputableℝSeq.instComputableOne = { one := ↑1 }

@[implicit_reducible]

instance ComputableℝSeq.instAdd : Add ComputableℝSeq

Equations

• ComputableℝSeq.instAdd = { add := ComputableℝSeq.add }

@[implicit_reducible]

instance ComputableℝSeq.instNeg : Neg ComputableℝSeq

Equations

• ComputableℝSeq.instNeg = { neg := ComputableℝSeq.neg }

@[implicit_reducible]

instance ComputableℝSeq.instSub : Sub ComputableℝSeq

Equations

• ComputableℝSeq.instSub = { sub := ComputableℝSeq.sub }

@[implicit_reducible]

instance ComputableℝSeq.instMul : Mul ComputableℝSeq

Equations

• ComputableℝSeq.instMul = { mul := ComputableℝSeq.mul }

@[implicit_reducible]

instance ComputableℝSeq.instInh : Inhabited ComputableℝSeq

Equations

• ComputableℝSeq.instInh = { default := 0 }

@[simp]

theorem ComputableℝSeq.natCast_lb {n : ℕ} : (↑n).lb = ↑n

@[simp]

theorem ComputableℝSeq.natCast_ub {n : ℕ} : (↑n).ub = ↑n

@[simp]

theorem ComputableℝSeq.val_natCast {n : ℕ} : (↑n).val = ↑n

@[simp]

theorem ComputableℝSeq.intCast_lb {z : ℤ} : (↑z).lb = ↑z

@[simp]

theorem ComputableℝSeq.intCast_ub {z : ℤ} : (↑z).ub = ↑z

@[simp]

theorem ComputableℝSeq.val_intCast {z : ℤ} : (↑z).val = ↑z

theorem ComputableℝSeq.ratCast_lb {q : ℚ} : (↑q).lb = CauSeq.const abs q

theorem ComputableℝSeq.ratCast_ub {q : ℚ} : (↑q).ub = CauSeq.const abs q

@[simp]

theorem ComputableℝSeq.val_ratCast {q : ℚ} : (↑q).val = ↑q

@[simp]

theorem ComputableℝSeq.zero_lb : lb 0 = 0

@[simp]

theorem ComputableℝSeq.zero_ub : ub 0 = 0

@[simp]

theorem ComputableℝSeq.val_zero : val 0 = 0

@[simp]

theorem ComputableℝSeq.one_lb : lb 1 = 1

@[simp]

theorem ComputableℝSeq.one_ub : ub 1 = 1

@[simp]

theorem ComputableℝSeq.val_one : val 1 = 1

@[simp]

theorem ComputableℝSeq.lb_add (x y : ComputableℝSeq) : (x + y).lb = x.lb + y.lb

@[simp]

theorem ComputableℝSeq.ub_add (x y : ComputableℝSeq) : (x + y).ub = x.ub + y.ub

@[simp]

theorem ComputableℝSeq.val_add (x y : ComputableℝSeq) : (x + y).val = x.val + y.val

@[simp]

theorem ComputableℝSeq.lb_neg (x : ComputableℝSeq) : (-x).lb = -x.ub

@[simp]

theorem ComputableℝSeq.ub_neg (x : ComputableℝSeq) : (-x).ub = -x.lb

@[simp]

theorem ComputableℝSeq.val_neg (x : ComputableℝSeq) : (-x).val = -x.val

@[simp]

theorem ComputableℝSeq.lb_sub (x y : ComputableℝSeq) : (x - y).lb = x.lb - y.ub

@[simp]

theorem ComputableℝSeq.ub_sub (x y : ComputableℝSeq) : (x - y).ub = x.ub - y.lb

@[simp]

theorem ComputableℝSeq.val_sub (x y : ComputableℝSeq) : (x - y).val = x.val - y.val

theorem ComputableℝSeq.lb_mul (x y : ComputableℝSeq) : (x * y).lb = x.lb * y.lb ⊓ x.ub * y.lb ⊓ (x.lb * y.ub ⊓ x.ub * y.ub)

theorem ComputableℝSeq.ub_mul (x y : ComputableℝSeq) : (x * y).ub = x.lb * y.lb ⊔ x.ub * y.lb ⊔ (x.lb * y.ub ⊔ x.ub * y.ub)

@[simp]

theorem ComputableℝSeq.val_mul (x y : ComputableℝSeq) : (x * y).val = x.val * y.val

noncomputable def ComputableℝSeq.sign (x : ComputableℝSeq) : SignType

The sign of x, defined classically as the sign of its real value, so this definition is noncomputable and carries no algorithmic content. (Searching the interval sequence for a sign witness terminates exactly when x ≠ 0 or some interval is the point 0, so a fuel-free executable version cannot be total.) This ends up providing the DecidableEq and DecidableLT instances on Computableℝ, which are likewise classical.

Equations

• x.sign = SignType.sign x.val

theorem ComputableℝSeq.sign_sound (x : ComputableℝSeq) : x.sign = SignType.sign x.val

theorem ComputableℝSeq.sign_pos_iff (x : ComputableℝSeq) : x.sign = SignType.pos ↔ 0 < x.val

theorem ComputableℝSeq.sign_neg_iff (x : ComputableℝSeq) : x.sign = SignType.neg ↔ x.val < 0

theorem ComputableℝSeq.sign_zero_iff (x : ComputableℝSeq) : x.sign = SignType.zero ↔ x.val = 0

noncomputable def ComputableℝSeq.signWitnessTerm (x : ComputableℝSeq) (hnz : x.val ≠ 0) : { xq : ℕ × ℚ // 0 < ↑xq.2 ∧ ↑xq.2 < |x.val| ∧ ∀ j ≥ xq.1, |↑(x.lb - x.ub) j| < xq.2 }

If x is nonzero, there is eventually a point in the Cauchy sequences where either the lower or upper bound prove this. This theorem states that this point exists.

Equations

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

theorem ComputableℝSeq.signWitnessTerm_prop (x : ComputableℝSeq) (n : ℕ) (hnz : x.val ≠ 0) (hub : ¬↑x.ub n < 0) (hlb : ¬↑x.lb n > 0) : n + Nat.succ 0 ≤ (↑(x.signWitnessTerm hnz)).1

theorem ComputableℝSeq.signWitness_def (x : ComputableℝSeq) (hnz : x.val ≠ 0) : x.signWitness hnz = definition.signWitness_aux✝ x 0 hnz

@[irreducible]

def ComputableℝSeq.signWitness (x : ComputableℝSeq) (hnz : x.val ≠ 0) : { n : ℕ // 0 < x.val ∧ 0 < ↑x.lb n ∨ x.val < 0 ∧ ↑x.ub n < 0 }

With the proof that x≠0, we can also eventually get a sign witness: a number n such that either 0 < x and 0 < lb n; or that x < 0 and ub n < 0. Marking it as irreducible because in theory all of the info needed is in the return Subtype.

Equations

• x.signWitness hnz = ComputableℝSeq.definition.signWitness_aux✝ x 0 hnz

def ComputableℝSeq.isPos {x : ComputableℝSeq} (hnz : x.val ≠ 0) : Bool

With the proof that x≠0, we get a total comparison function.

Equations

• ComputableℝSeq.isPos hnz = decide (0 < ↑x.lb ↑(x.signWitness hnz))

theorem ComputableℝSeq.isPos_iff (x : ComputableℝSeq) (hnz : x.val ≠ 0) : isPos hnz = true ↔ 0 < x.val

Proof that isPos correctly determines whether a nonzero computable number is positive.

theorem ComputableℝSeq.neg_of_not_pos {x : ComputableℝSeq} {hnz : x.val ≠ 0} (h : ¬isPos hnz = true) : x.val < 0

def ComputableℝSeq.dropTilSigned (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq

Given computable sequences for a nonzero x, drop the leading terms of both sequences (lb and ub) until both are nonzero. This gives a new sequence that we can "safely" invert.

Equations

• x.dropTilSigned hnz = ComputableℝSeq.mk x.val (fun (n : ℕ) => x.lub (↑(x.signWitness hnz) + n)) ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ComputableℝSeq.val_dropTilSigned {x : ComputableℝSeq} (h : x.val ≠ 0) : (x.dropTilSigned h).val = x.val

theorem ComputableℝSeq.dropTilSigned_nz {x : ComputableℝSeq} (h : x.val ≠ 0) : (x.dropTilSigned h).val ≠ 0

theorem ComputableℝSeq.sign_dropTilSigned {x : ComputableℝSeq} (hnz : x.val ≠ 0) : 0 < x.val ∧ 0 < ↑(x.dropTilSigned hnz).lb 0 ∨ x.val < 0 ∧ ↑(x.dropTilSigned hnz).ub 0 < 0

theorem ComputableℝSeq.dropTilSigned_pos {x : ComputableℝSeq} (h : x.val ≠ 0) : x.val > 0 ↔ ↑(x.dropTilSigned h).lb 0 > 0

theorem ComputableℝSeq.dropTilSigned_neg {x : ComputableℝSeq} (h : x.val ≠ 0) : x.val < 0 ↔ ↑(x.dropTilSigned h).ub 0 < 0

theorem ComputableℝSeq.neg_LimZero_lb_of_val {x : ComputableℝSeq} (hnz : x.val ≠ 0) : ¬x.lb.LimZero

theorem ComputableℝSeq.neg_LimZero_ub_of_val {x : ComputableℝSeq} (hnz : x.val ≠ 0) : ¬x.ub.LimZero

theorem ComputableℝSeq.pos_ub_of_val {x : ComputableℝSeq} (hp : x.val > 0) : x.ub.Pos

theorem ComputableℝSeq.pos_neg_ub_of_val {x : ComputableℝSeq} (hn : x.val < 0) : (-x.ub).Pos

theorem ComputableℝSeq.pos_lb_of_val {x : ComputableℝSeq} (hp : x.val > 0) : x.lb.Pos

theorem ComputableℝSeq.pos_neg_lb_of_val {x : ComputableℝSeq} (hn : x.val < 0) : (-x.lb).Pos

def ComputableℝSeq.lbInv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : CauSeq ℚ abs

The sequence of lower bounds of 1/x. Only functions "correctly" to give lower bounds if we assume that hx is already hx.dropTilSigned (as proven in lbInv_correct) -- but those assumptions aren't need for proving that it's Cauchy.

Equations

• x.lbInv hnz = if hp : ComputableℝSeq.isPos hnz = true then x.ub.inv ⋯ else let ub0 := ↑x.ub 0; ⟨fun (n : ℕ) => have ub := ↑x.ub n; if ub ≥ 0 then ub0⁻¹ else ub⁻¹, ⋯⟩

def ComputableℝSeq.ubInv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : CauSeq ℚ abs

Analgoous to lbInv for providing upper bounds on 1/x.

Equations

• x.ubInv hnz = if hp : ¬ComputableℝSeq.isPos hnz = true then x.lb.inv ⋯ else let lb0 := ↑x.lb 0; ⟨fun (n : ℕ) => have lb := ↑x.lb n; if lb ≤ 0 then lb0⁻¹ else lb⁻¹, ⋯⟩

theorem ComputableℝSeq.lbInv_correct {x : ComputableℝSeq} (hnz : x.val ≠ 0) (n : ℕ) : ↑(↑((x.dropTilSigned hnz).lbInv ⋯) n) ≤ x.val⁻¹

When applied to a dropTilSigned, lbInv is a correct lower bound on x⁻¹.

theorem ComputableℝSeq.ubInv_correct {x : ComputableℝSeq} (hnz : x.val ≠ 0) (n : ℕ) : ↑(↑((x.dropTilSigned hnz).ubInv ⋯) n) ≥ x.val⁻¹

When applied to a dropTilSigned, ubInv is a correct upper bound on x⁻¹.

theorem ComputableℝSeq.lbInv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : Real.mk (x.lbInv hnz) = x.val⁻¹

x.lbInv converges to (x.val)⁻¹.

theorem ComputableℝSeq.lbInv_signed_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : Real.mk ((x.dropTilSigned hnz).lbInv ⋯) = x.val⁻¹

When applied to a dropTilSigned, lbInv is converges to x⁻¹.

theorem ComputableℝSeq.ubInv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : Real.mk (x.ubInv hnz) = x.val⁻¹

x.ubInv converges to (x.val)⁻¹.

theorem ComputableℝSeq.ubInv_signed_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : Real.mk ((x.dropTilSigned hnz).ubInv ⋯) = x.val⁻¹

When applied to a dropTilSigned, ubInv is converges to x⁻¹. TODO: version without hnz hypothesis.

noncomputable def ComputableℝSeq.safeInv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq

An inverse is defined only on reals that we can prove are nonzero. If we can prove they are nonzero, then we can prove that at some point we learn the sign, and so can start giving actual upper and lower bounds. There is a separate inv that uses sign to construct the proof of nonzeroness by searching along the sequence (but isn't guaranteed to terminate).

Equations

• x.safeInv hnz = ComputableℝSeq.mk x.val⁻¹ (fun (n : ℕ) => { fst := ↑((x.dropTilSigned hnz).lbInv ⋯) n, snd := ↑((x.dropTilSigned hnz).ubInv ⋯) n, fst_le_snd := ⋯ }) ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ComputableℝSeq.val_safeInv {x : ComputableℝSeq} (hnz : x.val ≠ 0) : (x.safeInv hnz).val = x.val⁻¹

theorem ComputableℝSeq.val_safeInv_ne_zero {x : ComputableℝSeq} (hnz : x.val ≠ 0) : (x.safeInv hnz).val ≠ 0

def ComputableℝSeq.nzSeq : Type

Subtype of sequences with nonzero values. These admit a (terminating) inverse function.

Equations

• ComputableℝSeq.nzSeq = { x : ComputableℝSeq // x.val ≠ 0 }

noncomputable def ComputableℝSeq.invNz : nzSeq → nzSeq

The inverse on the subtype of sequences with nonzero value.

Equations

• ComputableℝSeq.invNz x = ⟨(↑x).safeInv ⋯, ⋯⟩

@[simp]

theorem ComputableℝSeq.val_invNz (x : nzSeq) : (↑(invNz x)).val = (↑x).val⁻¹

@[implicit_reducible]

noncomputable instance ComputableℝSeq.instNzInv : Inv nzSeq

Equations

• ComputableℝSeq.instNzInv = { inv := ComputableℝSeq.invNz }

noncomputable def ComputableℝSeq.inv : ComputableℝSeq → ComputableℝSeq

Inverse of a computable real. Will terminate if the argument is nonzero, or if it is zero and the upper and lower bounds become exactly zero at some point. See ComputableℝSeq.sign. If you want to only call this in a way guaranteed to terminate, use ComputableℝSeq.safeInv.

Equations

• x.inv = match h : x.sign with | SignType.pos => x.safeInv ⋯ | SignType.neg => x.safeInv ⋯ | SignType.zero => 0

@[implicit_reducible]

noncomputable instance ComputableℝSeq.instInv : Inv ComputableℝSeq

Equations

• ComputableℝSeq.instInv = { inv := ComputableℝSeq.inv }

@[implicit_reducible]

noncomputable instance ComputableℝSeq.instDiv : Div ComputableℝSeq

Equations

• ComputableℝSeq.instDiv = { div := fun (x y : ComputableℝSeq) => x * y⁻¹ }

theorem ComputableℝSeq.inv_def (x : ComputableℝSeq) : x⁻¹ = x.inv

theorem ComputableℝSeq.inv_eq_safeInv {x : ComputableℝSeq} (hnz : x.val ≠ 0) : x⁻¹ = x.safeInv hnz

The inverse is equal to the safeInv. This is an actual equality of sequences, not just equivalence.

@[simp]

theorem ComputableℝSeq.val_inv (x : ComputableℝSeq) : x⁻¹.val = x.val⁻¹

@[simp]

theorem ComputableℝSeq.val_div (x y : ComputableℝSeq) : (x / y).val = x.val / y.val

theorem ComputableℝSeq.add_comm (x y : ComputableℝSeq) : x + y = y + x

theorem ComputableℝSeq.mul_comm (x y : ComputableℝSeq) : x * y = y * x

theorem ComputableℝSeq.neg_mul (x y : ComputableℝSeq) : -x * y = -(x * y)

theorem ComputableℝSeq.mul_neg (x y : ComputableℝSeq) : x * -y = -(x * y)

theorem ComputableℝSeq.neg_eq_of_add (x y : ComputableℝSeq) (h : x + y = 0) : -x = y

class ComputableℝSeq.CompSeqClass (G : Type u) extends AddCommMonoid G, CommMagma G, MulZeroOneClass G, Inv G, Div G, HasDistribNeg G, SubtractionCommMonoid G, NatCast G, IntCast G, RatCast G : Type u

Computable sequences have most of the properties of a field, including negation, subtraction, multiplication, division, IntCast all working as one would expect, with commutativity/associativity, involutive negation, and distributive properties ... except for a few crucial facts that a - a ≠ 0, a * a⁻¹ ≠ 1, and (a⁻¹)⁻¹ ≠ a. This typeclass collects all these facts together.

TODO could include mul_inv_rev, inv_eq_of_mul, intCast_ofNat, intCast_negSucc.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : G) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : G) : a + b = b + a
• mul : G → G → G
• mul_comm (a b : G) : a * b = b * a
• one : G
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• zero_mul (a : G) : 0 * a = 0
• mul_zero (a : G) : a * 0 = 0
• inv : G → G
• div : G → G → G
• neg : G → G
• neg_neg (x : G) : - -x = x
• neg_mul (x y : G) : -x * y = -(x * y)
• mul_neg (x y : G) : x * -y = -(x * y)
• sub : G → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul : ℤ → G → G
• zsmul_zero' (a : G) : ComputableℝSeq.CompSeqClass.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : G) : ComputableℝSeq.CompSeqClass.zsmul (↑n.succ) a = ComputableℝSeq.CompSeqClass.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : G) : ComputableℝSeq.CompSeqClass.zsmul (Int.negSucc n) a = -ComputableℝSeq.CompSeqClass.zsmul (↑n.succ) a
• neg_add_rev (a b : G) : -(a + b) = -b + -a
• neg_eq_of_add (a b : G) : a + b = 0 → -a = b
• natCast : ℕ → G
• intCast : ℤ → G
• ratCast : ℚ → G

@[implicit_reducible]

noncomputable instance ComputableℝSeq.instSeqCompSeqClass : CompSeqClass ComputableℝSeq

Equations

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

@[implicit_reducible]

instance ComputableℝSeq.equiv : Setoid ComputableℝSeq

The equivalence relation on ComputableℝSeq's given by converging to the same real value.

Equations

• ComputableℝSeq.equiv = { r := fun (f g : ComputableℝSeq) => f.val = g.val, iseqv := ComputableℝSeq.equiv._proof_1 }

theorem ComputableℝSeq.equiv_iff {x y : ComputableℝSeq} : x ≈ y ↔ x.val = y.val