The IsComputable typeclass

IsComputable x packages a ComputableℝSeq converging to the real number x: an explicit sequence of rational interval approximations. Closure instances (for arithmetic, powers, scalar multiples) and Decidable instances for comparisons are provided, along with a tool for lifting continuous functions defined by locally-uniformly converging rational approximations.

Since a ComputableℝSeq is an arbitrary function ℕ → ℚInterval (with convergence proofs) rather than recursive data, this is not computability in the computable-analysis sense, and the comparison instances below are classical (noncomputable, via sign information on the limit).

class IsComputable (x : ℝ) : Type

Type class stating that x : ℝ carries a ComputableℝSeq: an explicit sequence of rational interval approximations converging to x. Like Decidable, it carries data with it, and classically every real number admits such a sequence; its value lies in the explicit approximations it provides, not in a computability guarantee.

• seq : ComputableℝSeq

  A computable sequence representing x.

• prop : (seq x).val = x

  The sequence converges to x.

@[reducible]

def IsComputable.liftEq {x y : ℝ} (h : x = y) : 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 { seq := sx, prop := hsx } = { seq := sx, prop := ⋯ }

@[reducible]

def IsComputable.lift {x : ℝ} (fr : ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq) (h : ∀ (a : ComputableℝSeq), (fs a).val = fr a.val) : IsComputable x → IsComputable (fr x)

Definition of lift.

Equations

• IsComputable.lift fr fs h { seq := sx, prop := hsx } = { seq := fs sx, prop := ⋯ }

@[reducible]

def IsComputable.lift₂ {x y : ℝ} (fr : ℝ → ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq) (h : ∀ (a b : ComputableℝSeq), (fs a b).val = fr a.val b.val) : IsComputable x → IsComputable y → IsComputable (fr x y)

Definition of lift₂.

Equations

• IsComputable.lift₂ fr fs h { seq := sx, prop := hsx } { seq := sx_1, prop := hsx_1 } = { seq := fs sx sx_1, prop := ⋯ }

@[instance_reducible]

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

Equations

• IsComputable.instComputableNat n = { seq := ComputableℝSeq.ofRat ↑n, prop := ⋯ }

@[instance_reducible]

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

Equations

• IsComputable.instComputableInt z = { seq := ComputableℝSeq.ofRat ↑z, prop := ⋯ }

@[instance_reducible]

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

Equations

• IsComputable.instComputableRat q = { seq := ComputableℝSeq.ofRat q, prop := ⋯ }

@[instance_reducible]

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

Equations

• IsComputable.instComputableOfNat1 = { seq := 1, prop := ComputableℝSeq.val_one }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• IsComputable.instComputableNeg x = IsComputable.lift Neg.neg (fun (x : ComputableℝSeq) => -x) ComputableℝSeq.val_neg hx

@[instance_reducible]

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

Equations

• IsComputable.instComputableInv x = IsComputable.lift Inv.inv (fun (x : ComputableℝSeq) => x⁻¹) ComputableℝSeq.val_inv hx

@[instance_reducible]

instance IsComputable.instComputableAdd {x y : ℝ} [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x + y)

Equations

• IsComputable.instComputableAdd = IsComputable.lift₂ HAdd.hAdd (fun (x1 x2 : ComputableℝSeq) => x1 + x2) ComputableℝSeq.val_add hx hy

@[instance_reducible]

instance IsComputable.instComputableSub {x y : ℝ} [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x - y)

Equations

• IsComputable.instComputableSub = IsComputable.lift₂ HSub.hSub (fun (x1 x2 : ComputableℝSeq) => x1 - x2) ComputableℝSeq.val_sub hx hy

@[instance_reducible]

instance IsComputable.instComputableMul {x y : ℝ} [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x * y)

Equations

• IsComputable.instComputableMul = IsComputable.lift₂ HMul.hMul (fun (x1 x2 : ComputableℝSeq) => x1 * x2) ComputableℝSeq.val_mul hx hy

@[instance_reducible]

noncomputable instance IsComputable.instComputableDiv {x y : ℝ} [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x / y)

Equations

• IsComputable.instComputableDiv = IsComputable.lift₂ HDiv.hDiv (fun (x1 x2 : ComputableℝSeq) => x1 / x2) ComputableℝSeq.val_div hx hy

@[instance_reducible]

instance IsComputable.instComputableNatPow {x : ℝ} [hx : IsComputable x] (n : ℕ) : IsComputable (x ^ n)

Equations

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

@[instance_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.

@[instance_reducible]

noncomputable instance IsComputable.instComputableNSMul {x : ℝ} [hx : IsComputable x] (n : ℕ) : IsComputable (n • x)

Equations

• IsComputable.instComputableNSMul n = IsComputable.lift (HSMul.hSMul n) (fun (x : ComputableℝSeq) => n • x) ⋯ hx

@[instance_reducible]

noncomputable instance IsComputable.instComputableZSMul {x : ℝ} [hx : IsComputable x] (z : ℤ) : IsComputable (z • x)

Equations

• IsComputable.instComputableZSMul z = ⋯.mpr inferInstance

@[instance_reducible]

noncomputable instance IsComputable.instComputableQSMul {x : ℝ} [hx : IsComputable x] (q : ℚ) : IsComputable (q • x)

Equations

• IsComputable.instComputableQSMul q = id inferInstance

@[instance_reducible]

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

When expressions happen to be IsComputable, we can get a decidability instance by lifting them to a comparison on the ComputableℝSeqs. The comparison there is classical (it goes through the noncomputable ComputableℝSeq.sign), so this instance is noncomputable and carries no algorithmic content.

Equations

• IsComputable.instDecidableLE = decidable_of_decidable_of_iff ⋯

@[instance_reducible]

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

Equations

• IsComputable.instDecidableEq = decidable_of_decidable_of_iff ⋯

@[instance_reducible]

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

Equations

• IsComputable.instDecidableLT = decidable_of_decidable_of_iff ⋯

@[instance_reducible]

noncomputable instance IsComputable.instDecidableLEval (x y : ComputableℝSeq) : Decidable (x.val ≤ y.val)

Equations

• IsComputable.instDecidableLEval x y = IsComputable.instDecidableLE

@[instance_reducible]

noncomputable instance IsComputable.instDecidableLTval (x y : ComputableℝSeq) : Decidable (x.val < y.val)

Equations

• IsComputable.instDecidableLTval x y = IsComputable.instDecidableLT

def TendstoLocallyUniformlyWithout (F : ℕ → ℚ → ℚ) (f : ℝ → ℝ) : Prop

This is very similar to the statement TendstoLocallyUniformly (fun n x ↦ (F n x : ℝ)) (fun (q : ℚ) ↦ f q) .atTop but that only uses neighborhoods within the rationals, which is a strictly weaker condition. This uses neighborhoods in the ambient space, the reals.

Equations

• TendstoLocallyUniformlyWithout F f = ∀ (ε : ℝ), 0 < ε → ∀ (x : ℝ), ∃ t ∈ nhds x, ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → ∀ (y : ℚ), ↑y ∈ t → |f ↑y - ↑(F b y)| < ε

theorem Real_mk_of_TendstoLocallyUniformly' (fImpl : ℕ → ℚ → ℚ) (f : ℝ → ℝ) (hfImpl : TendstoLocallyUniformlyWithout fImpl f) (hf : Continuous f) (x : CauSeq ℚ abs) : ∃ (h : IsCauSeq abs fun (n : ℕ) => fImpl n (↑x n)), Real.mk ⟨fun (n : ℕ) => fImpl n (↑x n), h⟩ = f (Real.mk x)

def ComputableℝSeq.ofTendstoLocallyUniformlyContinuous {f : ℝ → ℝ} (hf : Continuous f) (fImpl : ℕ → NonemptyInterval ℚ → NonemptyInterval ℚ) (fImpl_l fImpl_u : ℕ → ℚ → ℚ) (hlb : ∀ (n : ℕ) (q : NonemptyInterval ℚ), ∀ x ∈ q, ↑(fImpl_l n q.toProd.1) ≤ f x) (hub : ∀ (n : ℕ) (q : NonemptyInterval ℚ), ∀ x ∈ q, f x ≤ ↑(fImpl_u n q.toProd.2)) (hImplDef : ∀ (n : ℕ) (q : NonemptyInterval ℚ), fImpl n q = { fst := fImpl_l n q.toProd.1, snd := fImpl_u n q.toProd.2, fst_le_snd := ⋯ }) (hTLU_l : TendstoLocallyUniformlyWithout fImpl_l f) (hTLU_u : TendstoLocallyUniformlyWithout fImpl_u f) (x : ComputableℝSeq) : ComputableℝSeq

Definition of ofTendstoLocallyUniformlyContinuous.

Equations

• ComputableℝSeq.ofTendstoLocallyUniformlyContinuous hf fImpl fImpl_l fImpl_u hlb hub hImplDef hTLU_l hTLU_u x = ComputableℝSeq.mk (f x.val) (fun (n : ℕ) => fImpl n (x.lub n)) ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ComputableℝSeq.val_ofTendstoLocallyUniformlyContinuous (f : ℝ → ℝ) (hf : Continuous f) (fI : ℕ → NonemptyInterval ℚ → NonemptyInterval ℚ) (fl fu : ℕ → ℚ → ℚ) (h₁ : ∀ (n : ℕ) (q : NonemptyInterval ℚ), ∀ x ∈ q, ↑(fl n q.toProd.1) ≤ f x) (h₂ : ∀ (n : ℕ) (q : NonemptyInterval ℚ), ∀ x ∈ q, f x ≤ ↑(fu n q.toProd.2)) (h₃ : ∀ (n : ℕ) (q : NonemptyInterval ℚ), fI n q = { fst := fl n q.toProd.1, snd := fu n q.toProd.2, fst_le_snd := ⋯ }) (h₄ : TendstoLocallyUniformlyWithout fl f) (h₅ : TendstoLocallyUniformlyWithout fu f) (a : ComputableℝSeq) : (ofTendstoLocallyUniformlyContinuous hf fI fl fu h₁ h₂ h₃ h₄ h₅ a).val = f a.val

def Rat.toDecimal (q : ℚ) (prec : ℕ := 20) : String

Definition of toDecimal.

Equations

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