Analysis I, Section 6.3: Suprema and infima of sequences
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 Chapter6Definition 6.3.1
noncomputable abbrev Sequence.sup (a:Sequence) : EReal := sSup { x | ∃ n ≥ a.m, x = a n }Definition 6.3.1
noncomputable abbrev Sequence.inf (a:Sequence) : EReal := sInf { x | ∃ n ≥ a.m, x = a n }Example 6.3.3
example : ((fun (n:ℕ) ↦ (-1:ℝ)^(n+1)):Sequence).sup = 1 := ⊢ (↑fun n => (-1) ^ (n + 1)).sup = 1 All goals completed! 🐙Example 6.3.3
example : ((fun (n:ℕ) ↦ (-1:ℝ)^(n+1)):Sequence).inf = -1 := ⊢ (↑fun n => (-1) ^ (n + 1)).inf = -1 All goals completed! 🐙Example 6.3.4 / Exercise 6.3.1
example : ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)):Sequence).sup = 1 := ⊢ (↑fun n => 1 / (↑n + 1)).sup = 1 All goals completed! 🐙Example 6.3.4 / Exercise 6.3.1
example : ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)):Sequence).inf = 0 := ⊢ (↑fun n => 1 / (↑n + 1)).inf = 0 All goals completed! 🐙Example 6.3.5
example : ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).sup = ⊤ := ⊢ (↑fun n => ↑n + 1).sup = ⊤ All goals completed! 🐙Example 6.3.5
example : ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).inf = 1 := ⊢ (↑fun n => ↑n + 1).inf = 1 All 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 Mtheorem Sequence.bounded_iff (a:Sequence) : a.IsBounded ↔ a.BddAbove ∧ a.BddBelow := a:Sequence⊢ a.IsBounded ↔ a.BddAbove ∧ a.BddBelow All goals completed! 🐙theorem Sequence.sup_of_bounded {a:Sequence} (h: a.IsBounded) : a.sup.IsFinite := a:Sequenceh:a.IsBounded⊢ a.sup.IsFinite All goals completed! 🐙theorem Sequence.inf_of_bounded {a:Sequence} (h: a.IsBounded) : a.inf.IsFinite := a:Sequenceh:a.IsBounded⊢ a.inf.IsFinite All goals completed! 🐙Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2
theorem Sequence.le_sup {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≤ a.sup := a:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≤ a.sup All goals completed! 🐙Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2
theorem Sequence.sup_le_upper {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≤ M) : a.sup ≤ M := a:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≤ M⊢ a.sup ≤ M All goals completed! 🐙Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2
theorem Sequence.exists_between_lt_sup {a:Sequence} {y:EReal} (h: y < a.sup ) :
∃ n ≥ a.m, y < a n ∧ a n ≤ a.sup := a:Sequencey:ERealh:y < a.sup⊢ ∃ n ≥ a.m, y < ↑(a.seq n) ∧ ↑(a.seq n) ≤ a.sup All goals completed! 🐙Remark 6.3.7
theorem Sequence.ge_inf {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≥ a.inf := a:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≥ a.inf All goals completed! 🐙Remark 6.3.7
theorem Sequence.inf_ge_lower {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≥ M) : a.inf ≥ M := a:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≥ M⊢ a.inf ≥ M All goals completed! 🐙Remark 6.3.7
theorem Sequence.exists_between_gt_inf {a:Sequence} {y:EReal} (h: y > a.inf ) :
∃ n ≥ a.m, y > a n ∧ a n ≥ a.inf := a:Sequencey:ERealh:y > a.inf⊢ ∃ n ≥ a.m, y > ↑(a.seq n) ∧ ↑(a.seq n) ≥ a.inf All 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 nProposition 6.3.8 / Exercise 6.3.3
theorem Sequence.convergent_of_monotone {a:Sequence} (hbound: a.BddAbove) (hmono: a.IsMonotone) :
a.Convergent := a:Sequencehbound:a.BddAbovehmono:a.IsMonotone⊢ a.Convergent All goals completed! 🐙Proposition 6.3.8 / Exercise 6.3.3
theorem Sequence.lim_of_monotone {a:Sequence} (hbound: a.BddAbove) (hmono: a.IsMonotone) :
lim a = a.sup := a:Sequencehbound:a.BddAbovehmono:a.IsMonotone⊢ ↑(lim a) = a.sup All goals completed! 🐙theorem Sequence.convergent_of_antitone {a:Sequence} (hbound: a.BddBelow) (hmono: a.IsAntitone) :
a.Convergent := a:Sequencehbound:a.BddBelowhmono:a.IsAntitone⊢ a.Convergent All goals completed! 🐙theorem Sequence.lim_of_antitone {a:Sequence} (hbound: a.BddBelow) (hmono: a.IsAntitone) :
lim a = a.inf := a:Sequencehbound:a.BddBelowhmono:a.IsAntitone⊢ ↑(lim a) = a.inf All goals completed! 🐙theorem Sequence.convergent_iff_bounded_of_monotone {a:Sequence} (ha: a.IsMonotone) :
a.Convergent ↔ a.IsBounded := a:Sequenceha:a.IsMonotone⊢ a.Convergent ↔ a.IsBounded All goals completed! 🐙theorem Sequence.bounded_iff_convergent_of_antitone {a:Sequence} (ha: a.IsAntitone) :
a.Convergent ↔ a.IsBounded := a:Sequenceha:a.IsAntitone⊢ a.Convergent ↔ a.IsBounded All goals completed! 🐙
Example 6.3.9
example : (Example_6_3_9:Sequence).IsMonotone := ⊢ (↑Example_6_3_9).IsMonotone All goals completed! 🐙Example 6.3.9
example : (Example_6_3_9:Sequence).BddAboveBy 4 := ⊢ (↑Example_6_3_9).BddAboveBy 4 All goals completed! 🐙Example 6.3.9
example : (Example_6_3_9:Sequence).Convergent := ⊢ (↑Example_6_3_9).Convergent All goals completed! 🐙Example 6.3.9
example : lim (Example_6_3_9:Sequence) ≤ 4 := ⊢ lim ↑Example_6_3_9 ≤ 4 All goals completed! 🐙Proposition 6.3.1
theorem lim_of_exp {x:ℝ} (hpos: 0 < x) (hbound: x < 1) :
((fun (n:ℕ) ↦ x^n):Sequence).Convergent ∧ lim ((fun (n:ℕ) ↦ x^n):Sequence) = 0 := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0
-- This proof is written to follow the structure of the original text.
x:ℝhpos:0 < xhbound:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ n⊢ a.Convergent ∧ lim a = 0
x:ℝhpos:0 < xhbound:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorry⊢ a.Convergent ∧ lim a = 0
have hbound : a.BddBelowBy 0 := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 x:ℝhpos:0 < xhbound:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryn:ℤa✝:n ≥ a.m⊢ a.seq n ≥ 0; All goals completed! 🐙
have hbound' : a.BddBelow := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 All goals completed! 🐙
x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023⊢ a.Convergent ∧ lim a = 0
x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964⊢ a.Convergent ∧ L = 0
have : lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = x * L := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0
x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964⊢ (lim ↑fun n => x ^ (n + 1)) = lim (x • a); x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964⊢ (↑fun n => x ^ (n + 1)) = x • a; x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964⊢ (↑fun n => x ^ (n + 1)).m = (x • a).mx:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964n:ℤ⊢ (↑fun n => x ^ (n + 1)).seq n = (x • a).seq n; x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964n:ℤ⊢ (↑fun n => x ^ (n + 1)).seq n = (x • a).seq n
All goals completed! 🐙
have why2 : lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = lim ((fun (n:ℕ) ↦ x^n):Sequence) := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 All goals completed! 🐙
x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964this:(Chapter6.lim ↑fun n => _fvar.11822 ^ (n + 1)) = _fvar.11822 * _fvar.14163 := ?_mvar.14494why2:(Chapter6.lim ↑fun n => _fvar.11822 ^ (n + 1)) = Chapter6.lim ↑fun n => _fvar.11822 ^ n := ?_mvar.18928⊢ (lim ↑fun n => x ^ n) = 1 * Lx:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964this:(Chapter6.lim ↑fun n => _fvar.11822 ^ (n + 1)) = _fvar.11822 * _fvar.14163 := ?_mvar.14494why2:x * L = 1 * L⊢ a.Convergent ∧ L = 0; x:ℝhpos:0 < xhbound✝:x < 1a:Chapter6.Sequence := ↑fun n => _fvar.11822 ^ nwhy:Chapter6.Sequence.IsAntitone _fvar.11964 := sorryhbound:Chapter6.Sequence.BddBelowBy _fvar.11964 0 := ?_mvar.12054hbound':Chapter6.Sequence.BddBelow _fvar.11964 := ?_mvar.14129hconv:?_mvar.14152 := Chapter6.Sequence.convergent_of_antitone _fvar.14130 _fvar.12023L:ℝ := Chapter6.lim _fvar.11964this:(Chapter6.lim ↑fun n => _fvar.11822 ^ (n + 1)) = _fvar.11822 * _fvar.14163 := ?_mvar.14494why2:x * L = 1 * L⊢ a.Convergent ∧ L = 0
have hx : x ≠ 1 := x:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 All goals completed! 🐙
All goals completed! 🐙Exercise 6.3.4
theorem lim_of_exp' {x:ℝ} (hbound: x > 1) : ¬((fun (n:ℕ) ↦ x^n):Sequence).Convergent := x:ℝhbound:x > 1⊢ ¬(↑fun n => x ^ n).Convergent All goals completed! 🐙end Chapter6