Cauchy sequences

A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality. There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.

Important definitions

• IsCauSeq: a predicate that says f : ℕ → β→ β is Cauchy.
• CauSeq: the type of Cauchy sequences valued in type β with respect to an absolute value function abv.

Tags

sequence, cauchy, abs val, absolute value

ink

theorem exists_forall_ge_and {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {Q : α → Prop} : (∃ i, (j : α) → j ≥ i → P j) → (∃ i, (j : α) → j ≥ i → Q j) → ∃ i, ∀ (j : α), j ≥ i → P j ∧ Q j

ink

theorem rat_add_continuous_lemma {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] (abv : β → α) [inst : IsAbsoluteValue abv] {ε : α} (ε0 : 0 < ε) : ∃ δ, δ > 0 ∧ ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε

ink

theorem rat_mul_continuous_lemma {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] (abv : β → α) [inst : IsAbsoluteValue abv] {ε : α} {K₁ : α} {K₂ : α} (ε0 : 0 < ε) : ∃ δ, δ > 0 ∧ ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε

ink

theorem rat_inv_continuous_lemma {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] (abv : β → α) [inst : IsAbsoluteValue abv] {ε : α} {K : α} (ε0 : 0 < ε) (K0 : 0 < K) : ∃ δ, δ > 0 ∧ ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε

ink

def IsCauSeq {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] (abv : β → α) (f : ℕ → β) : Prop

A sequence is Cauchy if the distance between its entries tends to zero.

Equations

• IsCauSeq abv f = ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - f i) < ε

ink

theorem IsCauSeq.cauchy₂ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : ℕ → β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) : ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ i → abv (f j - f k) < ε

ink

theorem IsCauSeq.cauchy₃ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : ℕ → β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) : ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (f k - f j) < ε

ink

theorem IsCauSeq.add {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : ℕ → β} {g : ℕ → β} (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) : IsCauSeq abv (f + g)

ink

def CauSeq {α : Type u_1} [inst : LinearOrderedField α] (β : Type u_2) [inst : Ring β] (abv : β → α) : Type u_2

CauSeq β abv is the type of β-valued Cauchy sequences, with respect to the absolute value function abv.

Equations

• CauSeq β abv = { f // IsCauSeq abv f }

ink

instance CauSeq.instCoeFunCauSeqForAllNat {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} : CoeFun (CauSeq β abv) fun x => ℕ → β

Equations

• CauSeq.instCoeFunCauSeqForAllNat = { coe := Subtype.val }

ink

theorem CauSeq.ext {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} {f : CauSeq β abv} {g : CauSeq β abv} (h : ∀ (i : ℕ), ↑f i = ↑g i) : f = g

ink

theorem CauSeq.isCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} (f : CauSeq β abv) : IsCauSeq abv ↑f

ink

theorem CauSeq.cauchy {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} (f : CauSeq β abv) {ε : α} : 0 < ε → ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < ε

ink

def CauSeq.ofEq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} (f : CauSeq β abv) (g : ℕ → β) (e : ∀ (i : ℕ), ↑f i = g i) : CauSeq β abv

Given a Cauchy sequence f, create a Cauchy sequence from a sequence g with the same values as f.

Equations

• CauSeq.ofEq f g e = { val := g, property := (_ : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (g j - g i) < ε) }

ink

theorem CauSeq.cauchy₂ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} : 0 < ε → ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ i → abv (↑f j - ↑f k) < ε

ink

theorem CauSeq.cauchy₃ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} : 0 < ε → ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε

ink

theorem CauSeq.bounded {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) : ∃ r, ∀ (i : ℕ), abv (↑f i) < r

ink

theorem CauSeq.bounded' {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (x : α) : ∃ r, r > x ∧ ∀ (i : ℕ), abv (↑f i) < r

ink

instance CauSeq.instAddCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Add (CauSeq β abv)

Equations

• CauSeq.instAddCauSeq = { add := fun f g => { val := ↑f + ↑g, property := (_ : IsCauSeq abv (↑f + ↑g)) } }

ink

@[simp]

theorem CauSeq.coe_add {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) : ↑(f + g) = ↑f + ↑g

ink

@[simp]

theorem CauSeq.add_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ℕ) : ↑(f + g) i = ↑f i + ↑g i

ink

def CauSeq.const {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] (abv : β → α) [inst : IsAbsoluteValue abv] (x : β) : CauSeq β abv

The constant Cauchy sequence.

Equations

• CauSeq.const abv x = { val := fun x => x, property := (_ : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv ((fun x => x) j - (fun x => x) i) < ε) }

ink

@[simp]

theorem CauSeq.coe_const {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) : ↑(CauSeq.const abv x) = Function.const ℕ x

ink

@[simp]

theorem CauSeq.const_apply {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (i : ℕ) : ↑(CauSeq.const abv x) i = x

ink

theorem CauSeq.const_inj {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : β} {y : β} : CauSeq.const abv x = CauSeq.const abv y ↔ x = y

ink

instance CauSeq.instZeroCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Zero (CauSeq β abv)

Equations

• CauSeq.instZeroCauSeq = { zero := CauSeq.const abv 0 }

ink

instance CauSeq.instOneCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : One (CauSeq β abv)

Equations

• CauSeq.instOneCauSeq = { one := CauSeq.const abv 1 }

ink

instance CauSeq.instInhabitedCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Inhabited (CauSeq β abv)

Equations

• CauSeq.instInhabitedCauSeq = { default := 0 }

ink

@[simp]

theorem CauSeq.coe_zero {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : ↑0 = 0

ink

@[simp]

theorem CauSeq.coe_one {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : ↑1 = 1

ink

@[simp]

theorem CauSeq.zero_apply {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (i : ℕ) : ↑0 i = 0

ink

@[simp]

theorem CauSeq.one_apply {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (i : ℕ) : ↑1 i = 1

ink

@[simp]

theorem CauSeq.const_zero {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : CauSeq.const abv 0 = 0

ink

@[simp]

theorem CauSeq.const_one {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : CauSeq.const abv 1 = 1

ink

theorem CauSeq.const_add {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) : CauSeq.const abv (x + y) = CauSeq.const abv x + CauSeq.const abv y

ink

instance CauSeq.instMulCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Mul (CauSeq β abv)

Equations

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

ink

@[simp]

theorem CauSeq.coe_mul {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) : ↑(f * g) = ↑f * ↑g

ink

@[simp]

theorem CauSeq.mul_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ℕ) : ↑(f * g) i = ↑f i * ↑g i

ink

theorem CauSeq.const_mul {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) : CauSeq.const abv (x * y) = CauSeq.const abv x * CauSeq.const abv y

ink

instance CauSeq.instNegCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Neg (CauSeq β abv)

Equations

• CauSeq.instNegCauSeq = { neg := fun f => CauSeq.ofEq (CauSeq.const abv (-1) * f) (fun x => -↑f x) (_ : ∀ (i : ℕ), -1 * ↑f i = -↑f i) }

ink

@[simp]

theorem CauSeq.coe_neg {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) : ↑(-f) = -↑f

ink

@[simp]

theorem CauSeq.neg_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (i : ℕ) : ↑(-f) i = -↑f i

ink

theorem CauSeq.const_neg {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) : CauSeq.const abv (-x) = -CauSeq.const abv x

ink

instance CauSeq.instSubCauSeq {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Sub (CauSeq β abv)

Equations

• CauSeq.instSubCauSeq = { sub := fun f g => CauSeq.ofEq (f + -g) (fun x => ↑f x - ↑g x) (_ : ∀ (i : ℕ), ↑f i + -↑g i = ↑f i - ↑g i) }

ink

@[simp]

theorem CauSeq.coe_sub {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) : ↑(f - g) = ↑f - ↑g

ink

@[simp]

theorem CauSeq.sub_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ℕ) : ↑(f - g) i = ↑f i - ↑g i

ink

theorem CauSeq.const_sub {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) : CauSeq.const abv (x - y) = CauSeq.const abv x - CauSeq.const abv y

ink

instance CauSeq.instSMulCauSeq {α : Type u_1} {β : Type u_2} {G : Type u_3} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : SMul G β] [inst : IsScalarTower G β β] : SMul G (CauSeq β abv)

Equations

• CauSeq.instSMulCauSeq = { smul := fun a f => CauSeq.ofEq (CauSeq.const abv (a • 1) * f) (a • ↑f) (_ : ∀ (x : ℕ), a • 1 * ↑f x = a • ↑f x) }

ink

@[simp]

theorem CauSeq.coe_smul {α : Type u_1} {β : Type u_2} {G : Type u_3} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : SMul G β] [inst : IsScalarTower G β β] (a : G) (f : CauSeq β abv) : ↑(a • f) = a • ↑f

ink

@[simp]

theorem CauSeq.smul_apply {α : Type u_1} {β : Type u_2} {G : Type u_3} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : SMul G β] [inst : IsScalarTower G β β] (a : G) (f : CauSeq β abv) (i : ℕ) : ↑(a • f) i = a • ↑f i

ink

theorem CauSeq.const_smul {α : Type u_2} {β : Type u_1} {G : Type u_3} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : SMul G β] [inst : IsScalarTower G β β] (a : G) (x : β) : CauSeq.const abv (a • x) = a • CauSeq.const abv x

ink

instance CauSeq.instIsScalarTowerCauSeqInstSMulCauSeqToSMulInstMulCauSeq {α : Type u_1} {β : Type u_2} {G : Type u_3} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : SMul G β] [inst : IsScalarTower G β β] : IsScalarTower G (CauSeq β abv) (CauSeq β abv)

Equations

• @CauSeq.instIsScalarTowerCauSeqInstSMulCauSeqToSMulInstMulCauSeq = @CauSeq.instIsScalarTowerCauSeqInstSMulCauSeqToSMulInstMulCauSeq.proof_1

ink

instance CauSeq.addGroup {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : AddGroup (CauSeq β abv)

Equations

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

ink

instance CauSeq.instNatCast {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : NatCast (CauSeq β abv)

Equations

• CauSeq.instNatCast = { natCast := fun n => CauSeq.const abv ↑n }

ink

instance CauSeq.instIntCast {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : IntCast (CauSeq β abv)

Equations

• CauSeq.instIntCast = { intCast := fun n => CauSeq.const abv ↑n }

ink

instance CauSeq.addGroupWithOne {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : AddGroupWithOne (CauSeq β abv)

Equations

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

ink

instance CauSeq.instPowCauSeqNat {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Pow (CauSeq β abv) ℕ

Equations

• CauSeq.instPowCauSeqNat = { pow := fun f n => CauSeq.ofEq (npowRec n f) (fun i => ↑f i ^ n) (_ : ∀ (i : ℕ), ↑(npowRec n f) i = ↑f i ^ n) }

ink

@[simp]

theorem CauSeq.coe_pow {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (n : ℕ) : ↑(f ^ n) = ↑f ^ n

ink

@[simp]

theorem CauSeq.pow_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (n : ℕ) (i : ℕ) : ↑(f ^ n) i = ↑f i ^ n

ink

theorem CauSeq.const_pow {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (n : ℕ) : CauSeq.const abv (x ^ n) = CauSeq.const abv x ^ n

ink

instance CauSeq.ring {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Ring (CauSeq β abv)

Equations

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

ink

instance CauSeq.instCommRingCauSeqToRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : CommRing β] {abv : β → α} [inst : IsAbsoluteValue abv] : CommRing (CauSeq β abv)

Equations

• CauSeq.instCommRingCauSeqToRing = let src := CauSeq.ring; CommRing.mk (_ : ∀ (a b : CauSeq β abv), a * b = b * a)

ink

def CauSeq.LimZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} (f : CauSeq β abv) : Prop

LimZero f holds when f approaches 0.

Equations

• CauSeq.LimZero f = ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε

ink

theorem CauSeq.add_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) : CauSeq.LimZero (f + g)

ink

theorem CauSeq.mul_limZero_right {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) {g : CauSeq β abv} (hg : CauSeq.LimZero g) : CauSeq.LimZero (f * g)

ink

theorem CauSeq.mul_limZero_left {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (g : CauSeq β abv) (hg : CauSeq.LimZero f) : CauSeq.LimZero (f * g)

ink

theorem CauSeq.neg_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : CauSeq.LimZero f) : CauSeq.LimZero (-f)

ink

theorem CauSeq.sub_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) : CauSeq.LimZero (f - g)

ink

theorem CauSeq.limZero_sub_rev {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hfg : CauSeq.LimZero (f - g)) : CauSeq.LimZero (g - f)

ink

theorem CauSeq.zero_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : CauSeq.LimZero 0

ink

theorem CauSeq.const_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : β} : CauSeq.LimZero (CauSeq.const abv x) ↔ x = 0

ink

instance CauSeq.equiv {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] : Setoid (CauSeq β abv)

Equations

• CauSeq.equiv = { r := fun f g => CauSeq.LimZero (f - g), iseqv := (_ : Equivalence fun f g => CauSeq.LimZero (f - g)) }

ink

theorem CauSeq.add_equiv_add {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) : f1 + g1 ≈ f2 + g2

ink

theorem CauSeq.neg_equiv_neg {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : f ≈ g) : -f ≈ -g

ink

theorem CauSeq.sub_equiv_sub {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) : f1 - g1 ≈ f2 - g2

ink

theorem CauSeq.equiv_def₃ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (h : f ≈ g) {ε : α} (ε0 : 0 < ε) : ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑g j) < ε

ink

theorem CauSeq.limZero_congr {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (h : f ≈ g) : CauSeq.LimZero f ↔ CauSeq.LimZero g

ink

theorem CauSeq.abv_pos_of_not_limZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) : ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)

ink

theorem CauSeq.of_near {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : ℕ → β) (g : CauSeq β abv) (h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε) : IsCauSeq abv f

ink

theorem CauSeq.not_limZero_of_not_congr_zero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f ≈ 0) : ¬CauSeq.LimZero f

ink

theorem CauSeq.mul_equiv_zero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f ≈ 0) : g * f ≈ 0

ink

theorem CauSeq.mul_equiv_zero' {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f ≈ 0) : f * g ≈ 0

ink

theorem CauSeq.mul_not_equiv_zero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) : ¬f * g ≈ 0

ink

theorem CauSeq.const_equiv {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : β} {y : β} : CauSeq.const abv x ≈ CauSeq.const abv y ↔ x = y

ink

theorem CauSeq.mul_equiv_mul {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) : f1 * g1 ≈ f2 * g2

ink

theorem CauSeq.smul_equiv_smul {α : Type u_3} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {G : Type u_1} [inst : SMul G β] [inst : IsScalarTower G β β] {f1 : CauSeq β abv} {f2 : CauSeq β abv} (c : G) (hf : f1 ≈ f2) : c • f1 ≈ c • f2

ink

theorem CauSeq.pow_equiv_pow {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} (hf : f1 ≈ f2) (n : ℕ) : f1 ^ n ≈ f2 ^ n

ink

theorem CauSeq.one_not_equiv_zero {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : Ring β] [inst : IsDomain β] (abv : β → α) [inst : IsAbsoluteValue abv] : ¬CauSeq.const abv 1 ≈ CauSeq.const abv 0

ink

theorem CauSeq.inv_aux {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) (ε : α) : ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv ((↑f j)⁻¹ - (↑f i)⁻¹) < ε

ink

def CauSeq.inv {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (hf : ¬CauSeq.LimZero f) : CauSeq β abv

Given a Cauchy sequence f with nonzero limit, create a Cauchy sequence with values equal to the inverses of the values of f.

Equations

• CauSeq.inv f hf = { val := fun j => (↑f j)⁻¹, property := (_ : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv ((↑f j)⁻¹ - (↑f i)⁻¹) < ε) }

ink

@[simp]

theorem CauSeq.coe_inv {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) : ↑(CauSeq.inv f hf) = (↑f)⁻¹

ink

@[simp]

theorem CauSeq.inv_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) (i : ℕ) : ↑(CauSeq.inv f hf) i = (↑f i)⁻¹

ink

theorem CauSeq.inv_mul_cancel {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) : CauSeq.inv f hf * f ≈ 1

ink

theorem CauSeq.mul_inv_cancel {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) : f * CauSeq.inv f hf ≈ 1

ink

theorem CauSeq.const_inv {α : Type u_2} {β : Type u_1} [inst : LinearOrderedField α] [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : β} (hx : x ≠ 0) : CauSeq.const abv x⁻¹ = CauSeq.inv (CauSeq.const abv x) (_ : ¬CauSeq.LimZero (CauSeq.const abv x))

ink

def CauSeq.Pos {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) : Prop

The entries of a positive Cauchy sequence eventually have a positive lower bound.

Equations

• CauSeq.Pos f = ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑f j

ink

theorem CauSeq.not_limZero_of_pos {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} : CauSeq.Pos f → ¬CauSeq.LimZero f

ink

theorem CauSeq.const_pos {α : Type u_1} [inst : LinearOrderedField α] {x : α} : CauSeq.Pos (CauSeq.const abs x) ↔ 0 < x

ink

theorem CauSeq.add_pos {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} : CauSeq.Pos f → CauSeq.Pos g → CauSeq.Pos (f + g)

ink

theorem CauSeq.pos_add_limZero {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} : CauSeq.Pos f → CauSeq.LimZero g → CauSeq.Pos (f + g)

ink

theorem CauSeq.mul_pos {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} : CauSeq.Pos f → CauSeq.Pos g → CauSeq.Pos (f * g)

ink

theorem CauSeq.trichotomy {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) : CauSeq.Pos f ∨ CauSeq.LimZero f ∨ CauSeq.Pos (-f)

ink

instance CauSeq.instLTCauSeqToRingToDivisionRingToFieldAbsToHasAbsToNegToSupToSemilatticeSupToLatticeInstDistribLatticeToLinearOrderToLinearOrderedRingToLinearOrderedCommRing {α : Type u_1} [inst : LinearOrderedField α] : LT (CauSeq α abs)

Equations

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

ink

instance CauSeq.instLECauSeqToRingToDivisionRingToFieldAbsToHasAbsToNegToSupToSemilatticeSupToLatticeInstDistribLatticeToLinearOrderToLinearOrderedRingToLinearOrderedCommRing {α : Type u_1} [inst : LinearOrderedField α] : LE (CauSeq α abs)

Equations

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

ink

theorem CauSeq.lt_of_lt_of_eq {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f < g) (gh : g ≈ h) : f < h

ink

theorem CauSeq.lt_of_eq_of_lt {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f ≈ g) (gh : g < h) : f < h

ink

theorem CauSeq.lt_trans {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f < g) (gh : g < h) : f < h

ink

theorem CauSeq.lt_irrefl {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} : ¬f < f

ink

theorem CauSeq.le_of_eq_of_le {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (hfg : f ≈ g) (hgh : g ≤ h) : f ≤ h

ink

theorem CauSeq.le_of_le_of_eq {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (hfg : f ≤ g) (hgh : g ≈ h) : f ≤ h

ink

instance CauSeq.instPreorderCauSeqToRingToDivisionRingToFieldAbsToHasAbsToNegToSupToSemilatticeSupToLatticeInstDistribLatticeToLinearOrderToLinearOrderedRingToLinearOrderedCommRing {α : Type u_1} [inst : LinearOrderedField α] : Preorder (CauSeq α abs)

Equations

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

ink

theorem CauSeq.le_antisymm {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (fg : f ≤ g) (gf : g ≤ f) : f ≈ g

ink

theorem CauSeq.lt_total {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) : f < g ∨ f ≈ g ∨ g < f

ink

theorem CauSeq.le_total {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) : f ≤ g ∨ g ≤ f

ink

theorem CauSeq.const_lt {α : Type u_1} [inst : LinearOrderedField α] {x : α} {y : α} : CauSeq.const abs x < CauSeq.const abs y ↔ x < y

ink

theorem CauSeq.const_le {α : Type u_1} [inst : LinearOrderedField α] {x : α} {y : α} : CauSeq.const abs x ≤ CauSeq.const abs y ↔ x ≤ y

ink

theorem CauSeq.le_of_exists {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (h : ∃ i, ∀ (j : ℕ), j ≥ i → ↑f j ≤ ↑g j) : f ≤ g

ink

theorem CauSeq.exists_gt {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) : ∃ a, f < CauSeq.const abs a

ink

theorem CauSeq.exists_lt {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) : ∃ a, CauSeq.const abs a < f

ink

theorem CauSeq.rat_sup_continuous_lemma {α : Type u_1} [inst : LinearOrderedField α] {ε : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : abs (a₁ - b₁) < ε → abs (a₂ - b₂) < ε → abs (a₁ ⊔ a₂ - b₁ ⊔ b₂) < ε

ink

theorem CauSeq.rat_inf_continuous_lemma {α : Type u_1} [inst : LinearOrderedField α] {ε : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : abs (a₁ - b₁) < ε → abs (a₂ - b₂) < ε → abs (a₁ ⊓ a₂ - b₁ ⊓ b₂) < ε

ink

instance CauSeq.instSupCauSeqToRingToDivisionRingToFieldAbsToHasAbsToNegToSupToSemilatticeSupToLatticeInstDistribLatticeToLinearOrderToLinearOrderedRingToLinearOrderedCommRing {α : Type u_1} [inst : LinearOrderedField α] : Sup (CauSeq α abs)

Equations

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

ink

instance CauSeq.instInfCauSeqToRingToDivisionRingToFieldAbsToHasAbsToNegToSupToSemilatticeSupToLatticeInstDistribLatticeToLinearOrderToLinearOrderedRingToLinearOrderedCommRing {α : Type u_1} [inst : LinearOrderedField α] : Inf (CauSeq α abs)

Equations

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

ink

@[simp]

theorem CauSeq.coe_sup {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) : ↑(f ⊔ g) = ↑f ⊔ ↑g

ink

@[simp]

theorem CauSeq.coe_inf {α : Type u_1} [inst : LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) : ↑(f ⊓ g) = ↑f ⊓ ↑g

ink

theorem CauSeq.sup_limZero {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) : CauSeq.LimZero (f ⊔ g)

ink

theorem CauSeq.inf_limZero {α : Type u_1} [inst : LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) : CauSeq.LimZero (f ⊓ g)

ink

theorem CauSeq.sup_equiv_sup {α : Type u_1} [inst : LinearOrderedField α] {a₁ : CauSeq α abs} {b₁ : CauSeq α abs} {a₂ : CauSeq α abs} {b₂ : CauSeq α abs} (ha : a₁ ≈ a₂) (hb : b₁ ≈ b₂) : a₁ ⊔ b₁ ≈ a₂ ⊔ b₂

ink

theorem CauSeq.inf_equiv_inf {α : Type u_1} [inst : LinearOrderedField α] {a₁ : CauSeq α abs} {b₁ : CauSeq α abs} {a₂ : CauSeq α abs} {b₂ : CauSeq α abs} (ha : a₁ ≈ a₂) (hb : b₁ ≈ b₂) : a₁ ⊓ b₁ ≈ a₂ ⊓ b₂

ink

theorem CauSeq.sup_lt {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (ha : a < c) (hb : b < c) : a ⊔ b < c

ink

theorem CauSeq.lt_inf {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (hb : a < b) (hc : a < c) : a < b ⊓ c

ink

@[simp]

theorem CauSeq.sup_idem {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) : a ⊔ a = a

ink

@[simp]

theorem CauSeq.inf_idem {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) : a ⊓ a = a

ink

theorem CauSeq.sup_comm {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) : a ⊔ b = b ⊔ a

ink

theorem CauSeq.inf_comm {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) : a ⊓ b = b ⊓ a

ink

theorem CauSeq.sup_eq_right {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : a ≤ b) : a ⊔ b ≈ b

ink

theorem CauSeq.inf_eq_right {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : b ≤ a) : a ⊓ b ≈ b

ink

theorem CauSeq.sup_eq_left {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : b ≤ a) : a ⊔ b ≈ a

ink

theorem CauSeq.inf_eq_left {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : a ≤ b) : a ⊓ b ≈ a

ink

theorem CauSeq.le_sup_left {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} : a ≤ a ⊔ b

ink

theorem CauSeq.inf_le_left {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} : a ⊓ b ≤ a

ink

theorem CauSeq.le_sup_right {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} : b ≤ a ⊔ b

ink

theorem CauSeq.inf_le_right {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} : a ⊓ b ≤ b

ink

theorem CauSeq.sup_le {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (ha : a ≤ c) (hb : b ≤ c) : a ⊔ b ≤ c

ink

theorem CauSeq.le_inf {α : Type u_1} [inst : LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (hb : a ≤ b) (hc : a ≤ c) : a ≤ b ⊓ c

Note that DistribLattice (CauSeq α abs) is not true because there is no PartialOrder.

ink

theorem CauSeq.sup_inf_distrib_left {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) (c : CauSeq α abs) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

ink

theorem CauSeq.sup_inf_distrib_right {α : Type u_1} [inst : LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) (c : CauSeq α abs) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)