Аналіз I, Глава 6.1

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Definition of $ε$-closeness, $ε$-steadiness, and their eventual counterparts
• Notion of a Cauchy sequence, convergent sequence, and bounded sequence of reals

@[reducible, inline]

abbrev Real.close (ε x y : ℝ) : Prop

Equations

• ε.close x y = (dist x y ≤ ε)

theorem Real.close_def (ε x y : ℝ) : ε.close x y ↔ dist x y ≤ ε

Визначення 6.1.2 (ε-close). This is similar to the previous notion of ε-closeness, but where all quantities are real instead of rational.

structure Chapter6.Sequence : Type

Визначення 6.1.3 (Sequence). This is similar to the Chapter 5 sequence, except that now the sequence is real-valued. As with Chapter 5, we start sequences from 0 by default.

• m : ℤ
• seq : ℤ → ℝ
• vanish (n : ℤ) : n < self.m → self.seq n = 0

theorem Chapter6.Sequence.ext {x y : Sequence} (m : x.m = y.m) (seq : x.seq = y.seq) : x = y

theorem Chapter6.Sequence.ext_iff {x y : Sequence} : x = y ↔ x.m = y.m ∧ x.seq = y.seq

instance Chapter6.Sequence.instCoeFun : CoeFun Sequence fun (x : Sequence) => ℤ → ℝ

Sequences can be thought of as functions from ℤ to ℝ.

Equations

• Chapter6.Sequence.instCoeFun = { coe := fun (a : Chapter6.Sequence) => a.seq }

instance Chapter6.Sequence.instCoe : Coe (ℕ → ℝ) Sequence

Functions from ℕ to ℝ can be thought of as sequences.

Equations

• Chapter6.Sequence.instCoe = { coe := fun (a : ℕ → ℝ) => { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } }

@[reducible, inline]

abbrev Chapter6.Sequence.mk' (m : ℤ) (a : { n : ℤ // n ≥ m } → ℝ) : Sequence

Equations

• Chapter6.Sequence.mk' m a = { m := m, seq := fun (n : ℤ) => if h : n ≥ m then a ⟨n, h⟩ else 0, vanish := ⋯ }

theorem Chapter6.Sequence.eval_mk {n m : ℤ} (a : { n : ℤ // n ≥ m } → ℝ) (h : n ≥ m) : (mk' m a).seq n = a ⟨n, h⟩

@[simp]

theorem Chapter6.Sequence.eval_coe (n : ℕ) (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n

@[reducible, inline]

abbrev Chapter6.Sequence.from (a : Sequence) (m₁ : ℤ) : Sequence

a.from n₁ starts a:Sequence from n₁. It is intended for use when n₁ ≥ n₀, but returns the "junk" value of the original sequence a otherwise.

Equations

• a.from m₁ = Chapter6.Sequence.mk' (max a.m m₁) fun (n : { n : ℤ // n ≥ max a.m m₁ }) => a.seq ↑n

theorem Chapter6.Sequence.from_eval (a : Sequence) {m₁ n : ℤ} (hn : n ≥ m₁) : (a.from m₁).seq n = a.seq n

@[reducible, inline]

abbrev Real.steady (ε : ℝ) (a : Chapter6.Sequence) : Prop

Визначення 6.1.3 (ε-steady)

Equations

• ε.steady a = ∀ n ≥ a.m, ∀ m ≥ a.m, ε.close (a.seq n) (a.seq m)

theorem Real.steady_def (ε : ℝ) (a : Chapter6.Sequence) : ε.steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.close (a.seq n) (a.seq m)

Визначення 6.1.3 (ε-steady)

@[reducible, inline]

abbrev Real.eventuallySteady (ε : ℝ) (a : Chapter6.Sequence) : Prop

Визначення 6.1.3 (Eventually ε-steady)

Equations

• ε.eventuallySteady a = ∃ N ≥ a.m, ε.steady (a.from N)

theorem Real.eventuallySteady_def (ε : ℝ) (a : Chapter6.Sequence) : ε.eventuallySteady a ↔ ∃ N ≥ a.m, ε.steady (a.from N)

Визначення 6.1.3 (Eventually ε-steady)

theorem Real.steady_mono {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hsteady : ε₁.steady a) : ε₂.steady a

theorem Real.eventuallySteady_mono {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hsteady : ε₁.eventuallySteady a) : ε₂.eventuallySteady a

@[reducible, inline]

abbrev Chapter6.Sequence.isCauchy (a : Sequence) : Prop

Визначення 6.1.3 (Cauchy sequence)

Equations

• a.isCauchy = ∀ ε > 0, ε.eventuallySteady a

theorem Chapter6.Sequence.isCauchy_def (a : Sequence) : a.isCauchy ↔ ∀ ε > 0, ε.eventuallySteady a

Визначення 6.1.3 (Cauchy sequence)

theorem Chapter6.Sequence.isCauchy_of_coe (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε

theorem Chapter6.Sequence.isCauchy_of_mk {n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℝ) : (mk' n₀ a).isCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε

instance Chapter6.Chapter5.Sequence.inst_coe_sequence : Coe Chapter5.Sequence Sequence

Equations

• Chapter6.Chapter5.Sequence.inst_coe_sequence = { coe := fun (a : Chapter5.Sequence) => { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ } }

@[simp]

theorem Chapter6.Chapter5.coe_sequence_eval (a : Chapter5.Sequence) (n : ℤ) : { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }.seq n = ↑(a.seq n)

theorem Chapter6.Sequence.is_steady_of_rat (ε : ℚ) (a : Chapter5.Sequence) : ε.steady a ↔ (↑ε).steady { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }

theorem Chapter6.Sequence.is_eventuallySteady_of_rat (ε : ℚ) (a : Chapter5.Sequence) : ε.eventuallySteady a ↔ (↑ε).eventuallySteady { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }

theorem Chapter6.Sequence.isCauchy_of_rat (a : Chapter5.Sequence) : a.isCauchy ↔ { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }.isCauchy

Твердження 6.1.4

@[reducible, inline]

abbrev Real.close_seq (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : Prop

Визначення 6.1.5

Equations

• ε.close_seq a L = ∀ n ≥ a.m, ε.close (a.seq n) L

theorem Real.close_seq_def (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : ε.close_seq a L ↔ ∀ n ≥ a.m, dist (a.seq n) L ≤ ε

Визначення 6.1.5

@[reducible, inline]

abbrev Real.eventually_close (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : Prop

Визначення 6.1.5

Equations

• ε.eventually_close a L = ∃ N ≥ a.m, ε.close_seq (a.from N) L

theorem Real.eventually_close_def (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : ε.eventually_close a L ↔ ∃ N ≥ a.m, ε.close_seq (a.from N) L

Визначення 6.1.5

theorem Real.close_seq_mono {L : ℝ} {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hclose : ε₁.close_seq a L) : ε₂.close_seq a L

theorem Real.eventually_close_mono {L : ℝ} {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hclose : ε₁.eventually_close a L) : ε₂.eventually_close a L

@[reducible, inline]

abbrev Chapter6.Sequence.tendsTo (a : Sequence) (L : ℝ) : Prop

Equations

• a.tendsTo L = ∀ ε > 0, ε.eventually_close a L

theorem Chapter6.Sequence.tendsTo_def (a : Sequence) (L : ℝ) : a.tendsTo L ↔ ∀ ε > 0, ε.eventually_close a L

theorem Chapter6.Sequence.tendsTo_iff (a : Sequence) (L : ℝ) : a.tendsTo L ↔ ∀ ε > 0, ∃ (N : ℤ), ∀ n ≥ N, |a.seq n - L| ≤ ε

Вправа 6.1.2

@[reducible, inline]

noncomputable abbrev Chapter6.seq_6_1_6 : Sequence

Equations

• Chapter6.seq_6_1_6 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)) n.toNat else 0, vanish := Chapter6.seq_6_1_6._proof_5 }

theorem Chapter6.Sequence.tendsTo_unique (a : Sequence) {L L' : ℝ} (h : L ≠ L') : ¬(a.tendsTo L ∧ a.tendsTo L')

Твердження 6.1.7 (Uniqueness of limits)

@[reducible, inline]

abbrev Chapter6.Sequence.convergent (a : Sequence) : Prop

Визначення 6.1.8

Equations

• a.convergent = ∃ (L : ℝ), a.tendsTo L

theorem Chapter6.Sequence.convergent_def (a : Sequence) : a.convergent ↔ ∃ (L : ℝ), a.tendsTo L

Визначення 6.1.8

@[reducible, inline]

abbrev Chapter6.Sequence.divergent (a : Sequence) : Prop

Визначення 6.1.8

Equations

• a.divergent = ¬a.convergent

theorem Chapter6.Sequence.divergent_def (a : Sequence) : a.divergent ↔ ¬a.convergent

Визначення 6.1.8

@[reducible, inline]

noncomputable abbrev Chapter6.lim (a : Sequence) : ℝ

Визначення 6.1.8. We give the limit of a sequence the junk value of 0 if it is not convergent.

Equations

• Chapter6.lim a = if h : a.convergent then Exists.choose h else 0

theorem Chapter6.Sequence.lim_def {a : Sequence} (h : a.convergent) : a.tendsTo (lim a)

Визначення 6.1.8

theorem Chapter6.Sequence.lim_eq {a : Sequence} {L : ℝ} : a.tendsTo L ↔ a.convergent ∧ lim a = L

Визначення 6.1.8

theorem Chapter6.Sequence.lim_harmonic : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.convergent ∧ lim { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ } = 0

Твердження 6.1.11

theorem Chapter6.Sequence.Cauchy_of_convergent {a : Sequence} (h : a.convergent) : a.isCauchy

Твердження 6.1.12 / Вправа 6.1.5

theorem Chapter6.Sequence.lim_eq_LIM {a : ℕ → ℚ} (h : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : { m := { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.n₀, seq := fun (n : ℤ) => ↑({ n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n), vanish := ⋯ }.tendsTo (Chapter5.Real.equivR (Chapter5.LIM a))

Твердження 6.1.15 / Вправа 6.1.6 (Formal limits are genuine limits)

@[reducible, inline]

abbrev Chapter6.Sequence.BoundedBy (a : Sequence) (M : ℝ) : Prop

Визначення 6.1.16

Equations

• a.BoundedBy M = ∀ (n : ℤ), |a.seq n| ≤ M

theorem Chapter6.Sequence.BoundedBy_def (a : Sequence) (M : ℝ) : a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M

Визначення 6.1.16

@[reducible, inline]

abbrev Chapter6.Sequence.isBounded (a : Sequence) : Prop

Визначення 6.1.16

Equations

• a.isBounded = ∃ M ≥ 0, a.BoundedBy M

theorem Chapter6.Sequence.isBounded_def (a : Sequence) : a.isBounded ↔ ∃ M ≥ 0, a.BoundedBy M

Визначення 6.1.16

theorem Chapter6.Sequence.bounded_of_cauchy {a : Sequence} (h : a.isCauchy) : a.isBounded

theorem Chapter6.Sequence.bounded_of_convergent {a : Sequence} (h : a.convergent) : a.isBounded

Наслідок 6.1.17

instance Chapter6.Sequence.inst_add : Add Sequence

Equations

• Chapter6.Sequence.inst_add = { add := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n + b.seq n else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_add {a b : Sequence} (ha : a.convergent) (hb : b.convergent) : (a + b).convergent ∧ lim (a + b) = lim a + lim b

Теорема 6.1.19(a) (limit laws)

instance Chapter6.Sequence.inst_mul : Mul Sequence

Equations

• Chapter6.Sequence.inst_mul = { mul := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n * b.seq n else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_mul {a b : Sequence} (ha : a.convergent) (hb : b.convergent) : (a * b).convergent ∧ lim (a * b) = lim a * lim b

Теорема 6.1.19(b) (limit laws)

instance Chapter6.Sequence.inst_smul : SMul ℝ Sequence

Equations

• Chapter6.Sequence.inst_smul = { smul := fun (c : ℝ) (a : Chapter6.Sequence) => { m := a.m, seq := fun (n : ℤ) => c * a.seq n, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_smul (c : ℝ) {a : Sequence} (ha : a.convergent) : (c • a).convergent ∧ lim (c • a) = c * lim a

Теорема 6.1.19(c) (limit laws)

instance Chapter6.Sequence.inst_sub : Sub Sequence

Equations

• Chapter6.Sequence.inst_sub = { sub := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n - b.seq n else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_sub {a b : Sequence} (ha : a.convergent) (hb : b.convergent) : (a - b).convergent ∧ lim (a - b) = lim a - lim b

Теорема 6.1.19(d) (limit laws)

noncomputable instance Chapter6.Sequence.inst_inv : Inv Sequence

Equations

• Chapter6.Sequence.inst_inv = { inv := fun (a : Chapter6.Sequence) => { m := a.m, seq := fun (n : ℤ) => (a.seq n)⁻¹, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_inv {a : Sequence} (ha : a.convergent) (hnon : lim a ≠ 0) : a⁻¹.convergent ∧ lim a⁻¹ = (lim a)⁻¹

Теорема 6.1.19(e) (limit laws)

noncomputable instance Chapter6.Sequence.inst_div : Div Sequence

Equations

• Chapter6.Sequence.inst_div = { div := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n / b.seq n else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_div {a b : Sequence} (ha : a.convergent) (hb : b.convergent) (hnon : lim b ≠ 0) : (a / b).convergent ∧ lim (a / b) = lim a / lim b

Теорема 6.1.19(f) (limit laws)

instance Chapter6.Sequence.inst_max : Max Sequence

Equations

• Chapter6.Sequence.inst_max = { max := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then max (a.seq n) (b.seq n) else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_max {a b : Sequence} (ha : a.convergent) (hb : b.convergent) (hnon : lim b ≠ 0) : (a ⊔ b).convergent ∧ lim (a ⊔ b) = max (lim a) (lim b)

Теорема 6.1.19(g) (limit laws)

instance Chapter6.Sequence.inst_min : Min Sequence

Equations

• Chapter6.Sequence.inst_min = { min := fun (a b : Chapter6.Sequence) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then min (a.seq n) (b.seq n) else 0, vanish := ⋯ } }

theorem Chapter6.Sequence.lim_min {a b : Sequence} (ha : a.convergent) (hb : b.convergent) (hnon : lim b ≠ 0) : (a ⊓ b).convergent ∧ lim (a ⊓ b) = min (lim a) (lim b)

Теорема 6.1.19(h) (limit laws)

theorem Chapter6.Sequence.mono_if {a : ℕ → ℝ} (ha : ∀ (n : ℕ), a (n + 1) > a n) {n m : ℕ} (hnm : m > n) : a m > a n

Вправа 6.1.1

theorem Chapter6.Sequence.tendsTo_of_from {a : Sequence} {c : ℝ} (m : ℤ) : a.tendsTo c ↔ (a.from m).tendsTo c

Вправа 6.1.3

theorem Chapter6.Sequence.tendsTo_of_shift {a : Sequence} {c : ℝ} (k : ℕ) : a.tendsTo c ↔ (mk' a.m fun (n : { n : ℤ // n ≥ a.m }) => a.seq (↑n + ↑k)).tendsTo c

Вправа 6.1.4

theorem Chapter6.Sequence.isBounded_of_rat (a : Chapter5.Sequence) : a.isBounded ↔ { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }.isBounded

Вправа 6.1.7

theorem Chapter6.Sequence.lim_div_fail : ∃ (a : Sequence) (b : Sequence), a.convergent ∧ b.convergent ∧ lim b = 0 ∧ ¬((a / b).convergent ∧ lim (a / b) = lim a / lim b)

Вправа 6.1.9

theorem Chapter6.Chapter5.Sequence.isCauchy_iff (a : Chapter5.Sequence) : a.isCauchy ↔ ∀ ε > 0, ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, ↑|a.seq n - a.seq m| ≤ ε

Вправа 6.1.10