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

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:

Suprema and infima of sequences

namespace Chapter6

Визначення 6.3.1

noncomputable abbrev Sequence.sup (a:Sequence) : EReal := sSup { x | ∃ n ≥ a.m, x = a n }

Визначення 6.3.1

noncomputable abbrev Sequence.inf (a:Sequence) : EReal := sInf { x | ∃ n ≥ a.m, x = a n }

Приклад 6.3.3

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

Приклад 6.3.3

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

Приклад 6.3.4 / Вправа 6.3.1

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

Приклад 6.3.4 / Вправа 6.3.1

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

Приклад 6.3.5

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

Приклад 6.3.5

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

abbrev Sequence.bddAboveBy (a:Sequence) (M:ℝ) : Prop := ∀ n ≥ a.m, a n ≤ Mabbrev Sequence.bddAbove (a:Sequence) : Prop := ∃ M, a.bddAboveBy Mabbrev Sequence.bddBelowBy (a:Sequence) (M:ℝ) : Prop := ∀ n ≥ a.m, a n ≥ Mabbrev Sequence.bddBelow (a:Sequence) : Prop := ∃ M, a.bddBelowBy M

theorem declaration uses 'sorry'Sequence.bounded_iff (a:Sequence) : a.isBounded ↔ a.bddAbove ∧ a.bddBelow := bya:Sequence⊢ a.isBounded ↔ a.bddAbove ∧ a.bddBelow sorryAll goals completed! 🐙

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

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

Твердження 6.3.6 (Least upper bound property) / Вправа 6.3.2

theorem declaration uses 'sorry'Sequence.le_sup {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≤ a.sup := bya:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≤ a.sup sorryAll goals completed! 🐙

Твердження 6.3.6 (Least upper bound property) / Вправа 6.3.2

theorem declaration uses 'sorry'Sequence.sup_le_upper {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≤ M) : a.sup ≤ M := bya:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≤ M⊢ a.sup ≤ M sorryAll goals completed! 🐙

Твердження 6.3.6 (Least upper bound property) / Вправа 6.3.2

theorem declaration uses 'sorry'Sequence.exists_between_lt_sup {a:Sequence} {y:EReal} (h: y < a.sup ) :
    ∃ n ≥ a.m, y < a n ∧ a n ≤ a.sup := bya:Sequencey:ERealh:y < a.sup⊢ ∃ n ≥ a.m, y < ↑(a.seq n) ∧ ↑(a.seq n) ≤ a.sup sorryAll goals completed! 🐙

Ремарка 6.3.7

theorem declaration uses 'sorry'Sequence.ge_inf {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≥ a.inf := bya:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≥ a.inf sorryAll goals completed! 🐙

Ремарка 6.3.7

theorem declaration uses 'sorry'Sequence.inf_ge_lower {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≥ M) : a.inf ≥ M := bya:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≥ M⊢ a.inf ≥ M sorryAll goals completed! 🐙

Ремарка 6.3.7

theorem declaration uses 'sorry'Sequence.exists_between_gt_inf {a:Sequence} {y:EReal} (h: y > a.inf ) :
    ∃ n ≥ a.m, y > a n ∧ a n ≥ a.inf := bya:Sequencey:ERealh:y > a.inf⊢ ∃ n ≥ a.m, y > ↑(a.seq n) ∧ ↑(a.seq n) ≥ a.inf sorryAll goals completed! 🐙

abbrev Sequence.isMonotone (a:Sequence) : Prop := ∀ n ≥ a.m, a (n+1) ≥ a nabbrev Sequence.isAntitone (a:Sequence) : Prop := ∀ n ≥ a.m, a (n+1) ≤ a n

Твердження 6.3.8 / Вправа 6.3.3

theorem declaration uses 'sorry'Sequence.convergent_of_monotone {a:Sequence} (hbound: a.bddAbove) (hmono: a.isMonotone) :
    a.convergent := bya:Sequencehbound:a.bddAbovehmono:a.isMonotone⊢ a.convergent sorryAll goals completed! 🐙

Твердження 6.3.8 / Вправа 6.3.3

theorem declaration uses 'sorry'Sequence.lim_of_monotone {a:Sequence} (hbound: a.bddAbove) (hmono: a.isMonotone) :
    lim a = a.sup := bya:Sequencehbound:a.bddAbovehmono:a.isMonotone⊢ ↑(lim a) = a.sup sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.convergent_of_antitone {a:Sequence} (hbound: a.bddBelow) (hmono: a.isAntitone) :
    a.convergent := bya:Sequencehbound:a.bddBelowhmono:a.isAntitone⊢ a.convergent sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.lim_of_antitone {a:Sequence} (hbound: a.bddBelow) (hmono: a.isAntitone) :
    lim a = a.inf := bya:Sequencehbound:a.bddBelowhmono:a.isAntitone⊢ ↑(lim a) = a.inf sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.convergent_iff_bounded_of_monotone {a:Sequence} (ha: a.isMonotone) :
    a.convergent ↔ a.isBounded := bya:Sequenceha:a.isMonotone⊢ a.convergent ↔ a.isBounded sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.bounded_iff_convergent_of_antitone {a:Sequence} (ha: a.isAntitone) :
    a.convergent ↔ a.isBounded := bya:Sequenceha:a.isAntitone⊢ a.convergent ↔ a.isBounded sorryAll goals completed! 🐙

Приклад 6.3.9

noncomputable abbrev Example_6_3_9 (n:ℕ) := ⌊ Real.pi * 10^n ⌋ / (10:ℝ)^n

Приклад 6.3.9

declaration uses 'sorry'example : (Example_6_3_9:Sequence).isMonotone := by⊢ { m := 0, seq := fun n => if n ≥ 0 then Example_6_3_9 n.toNat else 0, vanish := ⋯ }.isMonotone sorryAll goals completed! 🐙

Приклад 6.3.9

declaration uses 'sorry'example : (Example_6_3_9:Sequence).bddAboveBy 4 := by⊢ { m := 0, seq := fun n => if n ≥ 0 then Example_6_3_9 n.toNat else 0, vanish := ⋯ }.bddAboveBy 4 sorryAll goals completed! 🐙

Приклад 6.3.9

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

Приклад 6.3.9

declaration uses 'sorry'example : lim (Example_6_3_9:Sequence) ≤ 4 := by⊢ lim { m := 0, seq := fun n => if n ≥ 0 then Example_6_3_9 n.toNat else 0, vanish := ⋯ } ≤ 4 sorryAll goals completed! 🐙

Твердження 6.3.1

theorem declaration uses 'sorry'lim_of_exp {x:ℝ} (hpos: 0 < x) (hbound: x < 1) :
    ((fun (n:ℕ) ↦ x^n):Sequence).convergent ∧ lim ((fun (n:ℕ) ↦ x^n):Sequence) = 0 := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  set a := ((fun (n:ℕ) ↦ x^n):Sequence)x:ℝhpos:0 < xhbound:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }⊢ a.convergent ∧ lim a = 0
  have why : a.isAntitone := sorryx:ℝhpos:0 < xhbound:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitone⊢ a.convergent ∧ lim a = 0
  have hbound : a.bddBelowBy 0 := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0
    intro n hnx:ℝhpos:0 < xhbound:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonen:ℤhn:n ≥ a.m⊢ a.seq n ≥ 0; positivityAll goals completed! 🐙
  have hbound' : a.bddBelow := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0 use 0All goals completed! 🐙
  have hconv := a.convergent_of_antitone hbound' whyx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergent⊢ a.convergent ∧ lim a = 0
  set L := lim ax:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim a⊢ a.convergent ∧ L = 0
  have : lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = x * L := calc
    _ = lim (x • ((fun (n:ℕ) ↦ x^n):Sequence)) := byx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim a⊢ lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0, vanish := ⋯ } =
  lim (x • { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ })
      congre_a.e_seqx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim a⊢ (fun n => if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0) = fun n =>
  x * { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.seq n; ext ne_a.e_seq.hx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim an:ℤ⊢ (if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0) =
  x * { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.seq n
      by_cases h: n ≥ 0posx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim an:ℤh:n ≥ 0⊢ (if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0) =
  x * { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.seq nnegx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim an:ℤh:¬n ≥ 0⊢ (if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0) =
  x * { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.seq n
      all_goals simp [h, pow_succ']All goals completed! 🐙
    _ = x * lim ((fun (n:ℕ) ↦ x^n):Sequence) := byx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim a⊢ lim (x • { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }) =
  x * lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }
      exact (Sequence.lim_smul x hconv).2All goals completed! 🐙
    _ = _ := rfl
  have why2 :lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = lim ((fun (n:ℕ) ↦ x^n):Sequence) := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0 sorryAll goals completed! 🐙
  rw [this] at why2x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim athis:lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0, vanish := ⋯ } = x * Lwhy2:x * L = lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }⊢ a.convergent ∧ L = 0
  change x * L = L at why2x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim athis:lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0, vanish := ⋯ } = x * Lwhy2:x * L = L⊢ a.convergent ∧ L = 0
  replace why2 : x * L = 1 * L := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0 simp [why2]All goals completed! 🐙
  have hx : x ≠ 1 := byx:ℝhpos:0 < xhbound:x < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧
  lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0 linarithAll goals completed! 🐙
  simp only [mul_eq_mul_right_iff, hx, false_or] at why2x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }why:a.isAntitonehbound:a.bddBelowBy 0hbound':a.bddBelowhconv:a.convergentL:ℝ := lim athis:lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ (n + 1)) n.toNat else 0, vanish := ⋯ } = x * Lhx:x ≠ 1why2:L = 0⊢ a.convergent ∧ L = 0
  simp [hconv, why2]All goals completed! 🐙

Вправа 6.3.4

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

end Chapter6