Аналіз 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

/- Definition 6.1.1 (Distance).  Here we use the Mathlib distance. -/
Real.dist_eq (x y : ℝ) : dist x y = |x - y|#check Real.dist_eq

Real.dist_eq (x y : ℝ) : dist x y = |x - y|

abbrev Real.close (ε x y : ℝ) : Prop := 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.

theorem Real.close_def (ε x y : ℝ) : ε.close x y ↔ dist x y ≤ ε := byε:ℝx:ℝy:ℝ⊢ ε.close x y ↔ dist x y ≤ ε rflAll goals completed! 🐙

namespace Chapter6

Визначення 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.

@[ext]
structure Sequence where
  m : ℤ
  seq : ℤ → ℝ
  vanish : ∀ n < m, seq n = 0

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

instance Sequence.instCoeFun : CoeFun Sequence (fun _ ↦ ℤ → ℝ) where
  coe := fun a ↦ a.seq

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

instance Sequence.instCoe : Coe (ℕ → ℝ) Sequence where
  coe := fun a ↦ {
    m := 0
    seq := fun n ↦ if n ≥ 0 then a n.toNat else 0
    vanish := bya:ℕ → ℝ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0
      intro n hna:ℕ → ℝn:ℤhn:n < 0⊢ (if n ≥ 0 then a n.toNat else 0) = 0
      simp [hn]All goals completed! 🐙
  }

abbrev Sequence.mk' (m:ℤ) (a: { n // n ≥ m } → ℝ) : Sequence where
  m := m
  seq := fun n ↦ if h : n ≥ m then a ⟨n, h⟩ else 0
  vanish := bym:ℤa:{ n // n ≥ m } → ℝ⊢ ∀ n < m, (if h : n ≥ m then a ⟨n, h⟩ else 0) = 0
    intro n hnm:ℤa:{ n // n ≥ m } → ℝn:ℤhn:n < m⊢ (if h : n ≥ m then a ⟨n, h⟩ else 0) = 0
    simp [hn]All goals completed! 🐙

lemma Sequence.eval_mk {n m:ℤ} (a: { n // n ≥ m } → ℝ) (h: n ≥ m) :
    (Sequence.mk' m a) n = a ⟨ n, h ⟩ := byn:ℤm:ℤa:{ n // n ≥ m } → ℝh:n ≥ m⊢ (mk' m a).seq n = a ⟨n, h⟩ simp [seq, h]All goals completed! 🐙

@[simp]
lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℝ) : (a:Sequence) n = a n := byn:ℕa:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n simp [seq]All goals completed! 🐙

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

abbrev Sequence.from (a:Sequence) (m₁:ℤ) : Sequence :=
  mk' (max a.m m₁) (fun n ↦ a (n:ℤ))

lemma Sequence.from_eval (a:Sequence) {m₁ n:ℤ} (hn: n ≥ m₁) :
  (a.from m₁) n = a n := bya:Sequencem₁:ℤn:ℤhn:n ≥ m₁⊢ (a.from m₁).seq n = a.seq n
  simp [Sequence.from, seq, hn]a:Sequencem₁:ℤn:ℤhn:n ≥ m₁⊢ n < a.m → 0 = a.seq n
  intro ha:Sequencem₁:ℤn:ℤhn:n ≥ m₁h:n < a.m⊢ 0 = a.seq n
  exact (a.vanish n h).symmAll goals completed! 🐙

end Chapter6

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

abbrev Real.steady (ε: ℝ) (a: Chapter6.Sequence) : Prop :=
  ∀ n ≥ a.m, ∀ m ≥ a.m, ε.close (a n) (a m)

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

lemma Real.steady_def (ε: ℝ) (a: Chapter6.Sequence) :
  ε.steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.close (a n) (a m) := byε:ℝa:Chapter6.Sequence⊢ ε.steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.close (a.seq n) (a.seq m) rflAll goals completed! 🐙

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

abbrev Real.eventuallySteady (ε: ℝ) (a: Chapter6.Sequence) : Prop :=
  ∃ N ≥ a.m, ε.steady (a.from N)

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

lemma Real.eventuallySteady_def (ε: ℝ) (a: Chapter6.Sequence) :
  ε.eventuallySteady a ↔ ∃ N, (N ≥ a.m) ∧ ε.steady (a.from N) := byε:ℝa:Chapter6.Sequence⊢ ε.eventuallySteady a ↔ ∃ N ≥ a.m, ε.steady (a.from N) rflAll goals completed! 🐙

theorem declaration uses 'sorry'Real.steady_mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂) (hsteady: ε₁.steady a) :
    ε₂.steady a := bya:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hsteady:ε₁.steady a⊢ ε₂.steady a sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.eventuallySteady_mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂)
  (hsteady: ε₁.eventuallySteady a) :
    ε₂.eventuallySteady a := bya:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hsteady:ε₁.eventuallySteady a⊢ ε₂.eventuallySteady a sorryAll goals completed! 🐙

namespace Chapter6

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

abbrev Sequence.isCauchy (a:Sequence) : Prop := ∀ ε > (0:ℝ), ε.eventuallySteady a

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

lemma Sequence.isCauchy_def (a:Sequence) :
  a.isCauchy ↔ ∀ ε > (0:ℝ), ε.eventuallySteady a := bya:Sequence⊢ a.isCauchy ↔ ∀ ε > 0, ε.eventuallySteady a rflAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.isCauchy_of_coe (a:ℕ → ℝ) :
    (a:Sequence).isCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε := bya:ℕ → ℝ⊢ { 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) ≤ ε sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.isCauchy_of_mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℝ) :
    (mk' n₀ a).isCauchy
    ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist (mk' n₀ a j) (mk' n₀ a k) ≤ ε := byn₀:ℤ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) ≤ ε sorryAll goals completed! 🐙

instance Chapter5.Sequence.inst_coe_sequence : Coe Chapter5.Sequence Sequence  where
  coe := fun a ↦ {
    m := a.n₀
    seq := fun n ↦ ((a n):ℝ)
    vanish := bya:Chapter5.Sequence⊢ ∀ n < a.n₀, ↑(a.seq n) = 0
      intro n hna:Chapter5.Sequencen:ℤhn:n < a.n₀⊢ ↑(a.seq n) = 0
      have := a.vanish n hna:Chapter5.Sequencen:ℤhn:n < a.n₀this:a.seq n = 0⊢ ↑(a.seq n) = 0
      simp [this]All goals completed! 🐙
  }

@[simp]
theorem Chapter5.coe_sequence_eval (a: Chapter5.Sequence) (n:ℤ) : (a:Sequence) n = (a n:ℝ) := rfl

theorem declaration uses 'sorry'Sequence.is_steady_of_rat (ε:ℚ) (a: Chapter5.Sequence) :
    ε.steady a ↔ (ε:ℝ).steady (a:Sequence) := byε:ℚa:Chapter5.Sequence⊢ ε.steady a ↔ (↑ε).steady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ } sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.is_eventuallySteady_of_rat (ε:ℚ) (a: Chapter5.Sequence) :
    ε.eventuallySteady a ↔ (ε:ℝ).eventuallySteady (a:Sequence) := byε:ℚa:Chapter5.Sequence⊢ ε.eventuallySteady a ↔ (↑ε).eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ } sorryAll goals completed! 🐙

Твердження 6.1.4

theorem Sequence.isCauchy_of_rat (a: Chapter5.Sequence) : a.isCauchy ↔ (a:Sequence).isCauchy := bya:Chapter5.Sequence⊢ a.isCauchy ↔ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  constructormpa:Chapter5.Sequence⊢ a.isCauchy → { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchympra:Chapter5.Sequence⊢ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy → a.isCauchy
  swapmpra:Chapter5.Sequence⊢ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy → a.isCauchympa:Chapter5.Sequence⊢ a.isCauchy → { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy
  .mpra:Chapter5.Sequence⊢ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy → a.isCauchy intro hmpra:Chapter5.Sequenceh:{ m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy⊢ a.isCauchy
    rw [isCauchy_def] at hmpra:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }⊢ a.isCauchy
    rw [Chapter5.Sequence.isCauchy_def]mpra:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }⊢ ∀ ε > 0, ε.eventuallySteady a
    intro ε hεmpra:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }ε:ℚhε:ε > 0⊢ ε.eventuallySteady a
    specialize h (ε:ℝ) (bya:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }ε:ℚhε:ε > 0⊢ ↑ε > 0 positivityAll goals completed! 🐙)
    rwa [is_eventuallySteady_of_rat]mpra:Chapter5.Sequenceε:ℚhε:ε > 0h:(↑ε).eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }⊢ (↑ε).eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  intro hmpa:Chapter5.Sequenceh:a.isCauchy⊢ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy
  rw [Chapter5.Sequence.isCauchy_def] at hmpa:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady a⊢ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isCauchy
  rw [isCauchy_def]mpa:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady a⊢ ∀ ε > 0, ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  intro ε hεmpa:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady aε:ℝhε:ε > 0⊢ ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  have : ∃ ε' > (0:ℚ), ε' < ε := exists_pos_rat_lt hεmpa:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady aε:ℝhε:ε > 0this:∃ ε' > 0, ↑ε' < ε⊢ ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  obtain ⟨ ε', hε', hlt ⟩ := thismp.intro.introa:Chapter5.Sequenceh:∀ ε > 0, ε.eventuallySteady aε:ℝhε:ε > 0ε':ℚhε':ε' > 0hlt:↑ε' < ε⊢ ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  specialize h ε' hε'mp.intro.introa:Chapter5.Sequenceε:ℝhε:ε > 0ε':ℚhε':ε' > 0hlt:↑ε' < εh:ε'.eventuallySteady a⊢ ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  rw [is_eventuallySteady_of_rat] at hmp.intro.introa:Chapter5.Sequenceε:ℝhε:ε > 0ε':ℚhε':ε' > 0hlt:↑ε' < εh:(↑ε').eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }⊢ ε.eventuallySteady { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }
  exact Real.eventuallySteady_mono (le_of_lt hlt) hAll goals completed! 🐙

end Chapter6

Визначення 6.1.5

abbrev Real.close_seq (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) : Prop := ∀ n ≥ a.m, ε.close (a n) L

Визначення 6.1.5

theorem Real.close_seq_def (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) :
  ε.close_seq a L ↔ ∀ n ≥ a.m, dist (a n) L ≤ ε := byε:ℝa:Chapter6.SequenceL:ℝ⊢ ε.close_seq a L ↔ ∀ n ≥ a.m, dist (a.seq n) L ≤ ε rflAll goals completed! 🐙

Визначення 6.1.5

abbrev Real.eventually_close (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) : Prop :=
  ∃ N ≥ a.m, ε.close_seq (a.from N) L

Визначення 6.1.5

theorem Real.eventually_close_def (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) :
  ε.eventually_close a L ↔ ∃ N, (N ≥ a.m) ∧ ε.close_seq (a.from N) L := byε:ℝa:Chapter6.SequenceL:ℝ⊢ ε.eventually_close a L ↔ ∃ N ≥ a.m, ε.close_seq (a.from N) L rflAll goals completed! 🐙

theorem declaration uses 'sorry'Real.close_seq_mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂)
  (hclose: ε₁.close_seq a L) :
    ε₂.close_seq a L := byL:ℝa:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hclose:ε₁.close_seq a L⊢ ε₂.close_seq a L sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.eventually_close_mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂)
  (hclose: ε₁.eventually_close a L) :
    ε₂.eventually_close a L := byL:ℝa:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hclose:ε₁.eventually_close a L⊢ ε₂.eventually_close a L sorryAll goals completed! 🐙

namespace Chapter6

abbrev Sequence.tendsTo (a:Sequence) (L:ℝ) : Prop :=
  ∀ ε > (0:ℝ), ε.eventually_close a L

theorem Sequence.tendsTo_def (a:Sequence) (L:ℝ) :
  a.tendsTo L ↔ ∀ ε > (0:ℝ), ε.eventually_close a L := bya:SequenceL:ℝ⊢ a.tendsTo L ↔ ∀ ε > 0, ε.eventually_close a L rflAll goals completed! 🐙

Вправа 6.1.2

theorem declaration uses 'sorry'Sequence.tendsTo_iff (a:Sequence) (L:ℝ) :
  a.tendsTo L ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| ≤ ε := bya:SequenceL:ℝ⊢ a.tendsTo L ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε sorryAll goals completed! 🐙

noncomputable abbrev seq_6_1_6 : Sequence := (fun (n:ℕ) ↦ 1-(10:ℝ)^(-(n:ℤ)-1):Sequence)

Приклади 6.1.6

declaration uses 'sorry'example : (0.1:ℝ).close_seq seq_6_1_6 1 := by⊢ Real.close_seq 0.1 seq_6_1_6 1 sorryAll goals completed! 🐙

Приклади 6.1.6

declaration uses 'sorry'example : ¬ (0.01:ℝ).close_seq seq_6_1_6 1 := by⊢ ¬Real.close_seq 1e-2 seq_6_1_6 1 sorryAll goals completed! 🐙

Приклади 6.1.6

declaration uses 'sorry'example : (0.01:ℝ).eventually_close seq_6_1_6 1 := by⊢ Real.eventually_close 1e-2 seq_6_1_6 1 sorryAll goals completed! 🐙

Приклади 6.1.6

declaration uses 'sorry'example : seq_6_1_6.tendsTo 1 := by⊢ seq_6_1_6.tendsTo 1 sorryAll goals completed! 🐙

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

theorem Sequence.tendsTo_unique (a:Sequence) {L L':ℝ} (h:L ≠ L') :
    ¬ (a.tendsTo L ∧ a.tendsTo L') := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.tendsTo L ∧ a.tendsTo L')
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  by_contra thisa:SequenceL:ℝL':ℝh:L ≠ L'this:a.tendsTo L ∧ a.tendsTo L'⊢ False
  obtain ⟨ hL, hL' ⟩ := thisintroa:SequenceL:ℝL':ℝh:L ≠ L'hL:a.tendsTo LhL':a.tendsTo L'⊢ False
  replace h : L - L' ≠ 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.tendsTo L ∧ a.tendsTo L') contrapose! ha:SequenceL:ℝL':ℝhL:a.tendsTo LhL':a.tendsTo L'h:L - L' = 0⊢ L = L'; linarithAll goals completed! 🐙
  replace h : |L-L'| > 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.tendsTo L ∧ a.tendsTo L') positivityAll goals completed! 🐙
  set ε := |L-L'| / 3introa:SequenceL:ℝL':ℝhL:a.tendsTo LhL':a.tendsTo L'h:|L - L'| > 0ε:ℝ := |L - L'| / 3⊢ False
  have hε : ε > 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.tendsTo L ∧ a.tendsTo L') positivityAll goals completed! 🐙
  rw [tendsTo_iff] at hL hL'introa:SequenceL:ℝL':ℝhL:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0⊢ False
  specialize hL ε hεintroa:SequenceL:ℝL':ℝhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0hL:∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε⊢ False
  obtain ⟨ N, hN ⟩ := hLintro.introa:SequenceL:ℝL':ℝhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε⊢ False
  specialize hL' ε hεintro.introa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εhL':∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ ε⊢ False
  obtain ⟨ M, hM ⟩ := hL'intro.intro.introa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ ε⊢ False
  set n := max N Mintro.intro.introa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ εn:ℤ := max N M⊢ False
  specialize hN n (le_max_left N M)intro.intro.introa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ εn:ℤ := max N MhN:|a.seq n - L| ≤ ε⊢ False
  specialize hM n (le_max_right N M)intro.intro.introa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ False
  have : |L-L'| ≤ 2 * |L-L'|/3 := calc
    _ = dist L L' := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ |L - L'| = dist L L' rw [Real.dist_eq]All goals completed! 🐙
    _ ≤ dist L (a.seq n) + dist (a.seq n) L' := dist_triangle _ _ _
    _ ≤ ε + ε := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε
      rw [←Real.dist_eq] at hN hMa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:dist (a.seq n) L ≤ εhM:dist (a.seq n) L' ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε
      rw [dist_comm] at hNa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:dist L (a.seq n) ≤ εhM:dist (a.seq n) L' ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε
      gcongrAll goals completed! 🐙
    _ = 2 * |L-L'|/3 := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ ε + ε = 2 * |L - L'| / 3
      simp [ε]a:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ |L - L'| / 3 + |L - L'| / 3 = 2 * |L - L'| / 3; ringAll goals completed! 🐙
  linarithAll goals completed! 🐙

Визначення 6.1.8

abbrev Sequence.convergent (a:Sequence) : Prop := ∃ L, a.tendsTo L

Визначення 6.1.8

theorem Sequence.convergent_def (a:Sequence) : a.convergent ↔ ∃ L, a.tendsTo L := bya:Sequence⊢ a.convergent ↔ ∃ L, a.tendsTo L rflAll goals completed! 🐙

Визначення 6.1.8

abbrev Sequence.divergent (a:Sequence) : Prop := ¬ a.convergent

Визначення 6.1.8

theorem Sequence.divergent_def (a:Sequence) : a.divergent ↔ ¬ a.convergent := bya:Sequence⊢ a.divergent ↔ ¬a.convergent rflAll goals completed! 🐙

open Classical in
/--
  Визначення 6.1.8.  We give the limit of a sequence the junk value of 0 if it is not convergent.
-/
noncomputable abbrev lim (a:Sequence) : ℝ := if h: a.convergent then h.choose else 0

Визначення 6.1.8

theorem Sequence.lim_def {a:Sequence} (h: a.convergent) : a.tendsTo (lim a) := bya:Sequenceh:a.convergent⊢ a.tendsTo (lim a)
  unfold lima:Sequenceh:a.convergent⊢ a.tendsTo (if h : a.convergent then Exists.choose h else 0)
  simp [h]a:Sequenceh:a.convergent⊢ a.tendsTo (Exists.choose ⋯)
  convert h.choose_specAll goals completed! 🐙

Визначення 6.1.8

theorem Sequence.lim_eq {a:Sequence} {L:ℝ} :
a.tendsTo L ↔ a.convergent ∧ lim a = L := bya:SequenceL:ℝ⊢ a.tendsTo L ↔ a.convergent ∧ lim a = L
  constructormpa:SequenceL:ℝ⊢ a.tendsTo L → a.convergent ∧ lim a = Lmpra:SequenceL:ℝ⊢ a.convergent ∧ lim a = L → a.tendsTo L
  .mpa:SequenceL:ℝ⊢ a.tendsTo L → a.convergent ∧ lim a = L intro hmpa:SequenceL:ℝh:a.tendsTo L⊢ a.convergent ∧ lim a = L
    by_contra! eqmpa:SequenceL:ℝh:a.tendsTo Leq:a.convergent → lim a ≠ L⊢ False
    have : a.convergent := bya:SequenceL:ℝ⊢ a.tendsTo L ↔ a.convergent ∧ lim a = L rw [convergent_def]a:SequenceL:ℝh:a.tendsTo Leq:a.convergent → lim a ≠ L⊢ ∃ L, a.tendsTo L; use LAll goals completed! 🐙
    replace eq := a.tendsTo_unique (eq this)mpa:SequenceL:ℝh:a.tendsTo Lthis:a.convergenteq:¬(a.tendsTo (lim a) ∧ a.tendsTo L)⊢ False
    replace this := lim_def thismpa:SequenceL:ℝh:a.tendsTo Leq:¬(a.tendsTo (lim a) ∧ a.tendsTo L)this:a.tendsTo (lim a)⊢ False
    tautoAll goals completed! 🐙
  intro ⟨ h, h' ⟩mpra:SequenceL:ℝh:a.convergenth':lim a = L⊢ a.tendsTo L
  convert lim_def hh.e'_2a:SequenceL:ℝh:a.convergenth':lim a = L⊢ L = lim a
  rw [h']All goals completed! 🐙

Твердження 6.1.11

theorem Sequence.lim_harmonic :
    ((fun (n:ℕ) ↦ (n+1:ℝ)⁻¹):Sequence).convergent ∧ lim ((fun (n:ℕ) ↦ (n+1:ℝ)⁻¹):Sequence) = 0 := by⊢ { 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
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  rw [←lim_eq, tendsTo_iff]⊢ ∀ ε > 0,
  ∃ N,
    ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  intro ε hεε:ℝhε:ε > 0⊢ ∃ N,
  ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  have : ∃ (N:ℤ), N > 1/ε := exists_int_gt (1 / ε)ε:ℝhε:ε > 0this:∃ N, ↑N > 1 / ε⊢ ∃ N,
  ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  obtain ⟨ N, hN ⟩ := thisintroε:ℝhε:ε > 0N:ℤhN:↑N > 1 / ε⊢ ∃ N,
  ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  use Nhε:ℝhε:ε > 0N:ℤhN:↑N > 1 / ε⊢ ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  intro n hnhε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ N⊢ |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  have hNpos : (N:ℝ) > 0 := by⊢ { 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 apply LT.lt.trans _ hNε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ N⊢ 0 < 1 / ε; positivityAll goals completed! 🐙
  simp at hNposhε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < N⊢ |{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.seq n - 0| ≤ ε
  have hnpos : n ≥ 0 := by⊢ { 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 linarithAll goals completed! 🐙
  simp [hnpos, abs_inv]hε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ |↑n.toNat + 1|⁻¹ ≤ ε
  calc
    _ ≤ (N:ℝ)⁻¹ := byε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ |↑n.toNat + 1|⁻¹ ≤ (↑N)⁻¹
      rw [inv_le_inv₀ (by positivity) (by positivity)]ε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑N ≤ |↑n.toNat + 1|
      calc
        _ ≤ (n:ℝ) := byε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑N ≤ ↑n simp [hn]All goals completed! 🐙
        _ = (n.toNat:ℤ) := byε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑n = ↑↑n.toNat simp [hnpos]All goals completed! 🐙
        _ = n.toNat := rfl
        _ ≤ (n.toNat:ℝ) + 1 := byε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑n.toNat ≤ ↑n.toNat + 1 linarithAll goals completed! 🐙
        _ ≤ _ := le_abs_self _
    _ ≤ ε := byε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ (↑N)⁻¹ ≤ ε
      rw [inv_le_comm₀ (by positivity) (by positivity)]ε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ ≤ ↑N
      apply le_of_lthabε:ℝhε:ε > 0N:ℤhN:↑N > 1 / εn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ < ↑N
      rw [gt_iff_lt, ←inv_eq_one_div _] at hNhabε:ℝhε:ε > 0N:ℤhN:ε⁻¹ < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ < ↑N
      assumptionAll goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.Cauchy_of_convergent {a:Sequence} (h:a.convergent) : a.isCauchy := bya:Sequenceh:a.convergent⊢ a.isCauchy
  sorryAll goals completed! 🐙

Приклад 6.1.13

declaration uses 'sorry'example : ¬ (0.1:ℝ).eventuallySteady ((fun n ↦ (-1:ℝ)^n):Sequence) := by⊢ ¬Real.eventuallySteady 0.1 { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

Приклад 6.1.13

declaration uses 'sorry'example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).isCauchy := by⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.isCauchy sorryAll goals completed! 🐙

Приклад 6.1.13

declaration uses 'sorry'example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).convergent := by⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.convergent sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.lim_eq_LIM {a:ℕ → ℚ} (h: (a:Chapter5.Sequence).isCauchy) :
    ((a:Chapter5.Sequence):Sequence).tendsTo (Chapter5.Real.equivR (Chapter5.LIM a)) := bya:ℕ → ℚ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)) sorryAll goals completed! 🐙

Визначення 6.1.16

abbrev Sequence.BoundedBy (a:Sequence) (M:ℝ) : Prop :=
  ∀ n, |a n| ≤ M

Визначення 6.1.16

lemma Sequence.BoundedBy_def (a:Sequence) (M:ℝ) :
  a.BoundedBy M ↔ ∀ n, |a n| ≤ M := bya:SequenceM:ℝ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M rflAll goals completed! 🐙

Визначення 6.1.16

abbrev Sequence.isBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

Визначення 6.1.16

lemma Sequence.isBounded_def (a:Sequence) :
  a.isBounded ↔ ∃ M ≥ 0, a.BoundedBy M := bya:Sequence⊢ a.isBounded ↔ ∃ M ≥ 0, a.BoundedBy M rflAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.bounded_of_cauchy {a:Sequence} (h: a.isCauchy) : a.isBounded := bya:Sequenceh:a.isCauchy⊢ a.isBounded
  sorryAll goals completed! 🐙

Наслідок 6.1.17

theorem declaration uses 'sorry'Sequence.bounded_of_convergent {a:Sequence} (h: a.convergent) : a.isBounded := bya:Sequenceh:a.convergent⊢ a.isBounded
  sorryAll goals completed! 🐙

Приклад 6.1.18

declaration uses 'sorry'example : ¬ ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).isBounded := by⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => ↑n + 1) n.toNat else 0, vanish := ⋯ }.isBounded sorryAll goals completed! 🐙

Приклад 6.1.18

declaration uses 'sorry'example : ¬ ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).convergent := by⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => ↑n + 1) n.toNat else 0, vanish := ⋯ }.convergent sorryAll goals completed! 🐙

instance Sequence.inst_add : Add Sequence where
  add a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then a n + b n else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_add {a b:Sequence} (ha: a.convergent) (hb: b.convergent) :
    (a + b).convergent ∧ lim (a + b) = lim a + lim b := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergent⊢ (a + b).convergent ∧ lim (a + b) = lim a + lim b
  sorryAll goals completed! 🐙

instance Sequence.inst_mul : Mul Sequence where
  mul a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then a n * b n else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then a.seq n * b.seq n else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n * b.seq n else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n * b.seq n else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_mul {a b:Sequence} (ha: a.convergent) (hb: b.convergent) :
    (a * b).convergent ∧ lim (a * b) = lim a * lim b := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergent⊢ (a * b).convergent ∧ lim (a * b) = lim a * lim b
  sorryAll goals completed! 🐙

instance Sequence.inst_smul : SMul ℝ Sequence where
  smul c a := {
    m := a.m
    seq := fun (n:ℤ) ↦ c * a n
    vanish := byc:ℝa:Sequence⊢ ∀ n < a.m, c * a.seq n = 0
      intro n hnc:ℝa:Sequencen:ℤhn:n < a.m⊢ c * a.seq n = 0
      simp [a.vanish n hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_smul (c:ℝ) {a:Sequence} (ha: a.convergent) :
    (c • a).convergent ∧ lim (c • a) = c * lim a := byc:ℝa:Sequenceha:a.convergent⊢ (c • a).convergent ∧ lim (c • a) = c * lim a
  sorryAll goals completed! 🐙

instance Sequence.inst_sub : Sub Sequence where
  sub a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then a n - b n else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then a.seq n - b.seq n else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n - b.seq n else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n - b.seq n else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_sub {a b:Sequence} (ha: a.convergent) (hb: b.convergent) :
    (a - b).convergent ∧ lim (a - b) = lim a - lim b := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergent⊢ (a - b).convergent ∧ lim (a - b) = lim a - lim b
  sorryAll goals completed! 🐙

noncomputable instance Sequence.inst_inv : Inv Sequence where
  inv a := {
    m := a.m
    seq := fun (n:ℤ) ↦ (a n)⁻¹
    vanish := bya:Sequence⊢ ∀ n < a.m, (a.seq n)⁻¹ = 0
      intro n hna:Sequencen:ℤhn:n < a.m⊢ (a.seq n)⁻¹ = 0
      simp [a.vanish n hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_inv {a:Sequence} (ha: a.convergent) (hnon: lim a ≠ 0) :
  (a⁻¹).convergent ∧ lim (a⁻¹) = (lim a)⁻¹ := bya:Sequenceha:a.convergenthnon:lim a ≠ 0⊢ a⁻¹.convergent ∧ lim a⁻¹ = (lim a)⁻¹
  sorryAll goals completed! 🐙

noncomputable instance Sequence.inst_div : Div Sequence where
  div a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then a n / b n else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then a.seq n / b.seq n else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n / b.seq n else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n / b.seq n else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'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 := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergenthnon:lim b ≠ 0⊢ (a / b).convergent ∧ lim (a / b) = lim a / lim b
  sorryAll goals completed! 🐙

instance Sequence.inst_max : Max Sequence where
  max a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then max (a n) (b n) else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then max (a.seq n) (b.seq n) else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then max (a.seq n) (b.seq n) else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then max (a.seq n) (b.seq n) else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_max {a b:Sequence} (ha: a.convergent) (hb: b.convergent) (hnon: lim b ≠ 0) :
    (max a b).convergent ∧ lim (max a b) = max (lim a) (lim b) := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergenthnon:lim b ≠ 0⊢ (a ⊔ b).convergent ∧ lim (a ⊔ b) = max (lim a) (lim b)
  sorryAll goals completed! 🐙

instance Sequence.inst_min : Min Sequence where
  min a b := {
    m := max a.m b.m
    seq := fun (n:ℤ) ↦ if n ≥ max a.m b.m then min (a n) (b n) else 0
    vanish := bya:Sequenceb:Sequence⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then min (a.seq n) (b.seq n) else 0) = 0
      intro n hna:Sequenceb:Sequencen:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then min (a.seq n) (b.seq n) else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequenceb:Sequencen:ℤhn:¬n ≥ max a.m b.m⊢ (if n ≥ max a.m b.m then min (a.seq n) (b.seq n) else 0) = 0
      simp [hn]All goals completed! 🐙
  }

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

theorem declaration uses 'sorry'Sequence.lim_min {a b:Sequence} (ha: a.convergent) (hb: b.convergent) (hnon: lim b ≠ 0) :
    (min a b).convergent ∧ lim (min a b) = min (lim a) (lim b) := bya:Sequenceb:Sequenceha:a.convergenthb:b.convergenthnon:lim b ≠ 0⊢ (a ⊓ b).convergent ∧ lim (a ⊓ b) = min (lim a) (lim b)
  sorryAll goals completed! 🐙

Вправа 6.1.1

theorem declaration uses 'sorry'Sequence.mono_if {a: ℕ → ℝ} (ha: ∀ n, a (n+1) > a n) {n m:ℕ} (hnm: m > n) : a m > a n := bya:ℕ → ℝha:∀ (n : ℕ), a (n + 1) > a nn:ℕm:ℕhnm:m > n⊢ a m > a n
  sorryAll goals completed! 🐙

Вправа 6.1.3

theorem declaration uses 'sorry'Sequence.tendsTo_of_from {a: Sequence} {c:ℝ} (m:ℤ) :
    a.tendsTo c ↔ (a.from m).tendsTo c := bya:Sequencec:ℝm:ℤ⊢ a.tendsTo c ↔ (a.from m).tendsTo c
  sorryAll goals completed! 🐙

Вправа 6.1.4

theorem declaration uses 'sorry'Sequence.tendsTo_of_shift {a: Sequence} {c:ℝ} (k:ℕ) :
    a.tendsTo c ↔ (Sequence.mk' a.m (fun n : {n // n ≥ a.m} ↦ a (n+k))).tendsTo c := bya:Sequencec:ℝk:ℕ⊢ a.tendsTo c ↔ (mk' a.m fun n => a.seq (↑n + ↑k)).tendsTo c
  sorryAll goals completed! 🐙

Вправа 6.1.7

theorem declaration uses 'sorry'Sequence.isBounded_of_rat (a: Chapter5.Sequence) :
    a.isBounded ↔ (a:Sequence).isBounded := bya:Chapter5.Sequence⊢ a.isBounded ↔ { m := a.n₀, seq := fun n => ↑(a.seq n), vanish := ⋯ }.isBounded
  sorryAll goals completed! 🐙

Вправа 6.1.9

theorem declaration uses 'sorry'Sequence.lim_div_fail :
    ∃ a b, a.convergent
    ∧ b.convergent
    ∧ lim b = 0
    ∧ ¬ ((a / b).convergent ∧ lim (a / b) = lim a / lim b) := by⊢ ∃ a b, a.convergent ∧ b.convergent ∧ lim b = 0 ∧ ¬((a / b).convergent ∧ lim (a / b) = lim a / lim b)
  sorryAll goals completed! 🐙

Вправа 6.1.10

theorem declaration uses 'sorry'Chapter5.Sequence.isCauchy_iff (a:Chapter5.Sequence) :
    a.isCauchy ↔ ∀ ε > (0:ℝ), ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, |a n - a m| ≤ ε := bya:Chapter5.Sequence⊢ a.isCauchy ↔ ∀ ε > 0, ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, ↑|a.seq n - a.seq m| ≤ ε
  sorryAll goals completed! 🐙

end Chapter6