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

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:

• Formal series and their limits

• Absolute convergence; basic series laws.

namespace Chapter7open BigOperators @[simp] theorem Series.eval_coe (a : ℕ → ℝ) (n : ℕ) : (a : Series).seq n = a n := bya:ℕ → ℝn:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n simpAll goals completed! 🐙abbrev Series.mk' {m:ℤ} (a: { n // n ≥ m } → ℝ) : Series 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! 🐙theorem Series.eval_mk' {m:ℤ} (a : { n // n ≥ m } → ℝ) {n : ℤ} (h:n ≥ m) : (Series.mk' a).seq n = a ⟨ n, h ⟩ := bym:ℤa:{ n // n ≥ m } → ℝn:ℤh:n ≥ m⊢ (mk' a).seq n = a ⟨n, h⟩ simp [h]All goals completed! 🐙 theorem Series.partial_succ (s : Series) {N:ℤ} (h: N ≥ s.m-1) : s.partial (N+1) = s.partial N + s.seq (N+1) := bys:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) unfold Series.partials:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = ∑ n ∈ Finset.Icc s.m N, s.seq n + s.seq (N + 1) rw [add_comm (s.partial N) _]s:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = s.seq (N + 1) + s.partial N have : N+1 ∉ Finset.Icc s.m N := bys:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) simpAll goals completed! 🐙 convert Finset.sum_insert thish.e'_2.hs:SeriesN:ℤh:N ≥ s.m - 1this:N + 1 ∉ Finset.Icc s.m N⊢ Finset.Icc s.m (N + 1) = insert (N + 1) (Finset.Icc s.m N) refine (Finset.insert_Icc_right_eq_Icc_add_one ?_).symmh.e'_2.hs:SeriesN:ℤh:N ≥ s.m - 1this:N + 1 ∉ Finset.Icc s.m N⊢ s.m ≤ N + 1 linarithAll goals completed! 🐙abbrev Series.convergesTo (s : Series) (L:ℝ) : Prop := Filter.Tendsto (s.partial) Filter.atTop (nhds L)abbrev Series.converges (s : Series) : Prop := ∃ L, s.convergesTo Labbrev Series.diverges (s : Series) : Prop := ¬s.convergesopen Classical in noncomputable abbrev Series.sum (s : Series) : ℝ := if h : s.converges then h.choose else 0theorem Series.converges_of_convergesTo {s : Series} {L:ℝ} (h: s.convergesTo L) : s.converges := bys:SeriesL:ℝh:s.convergesTo L⊢ s.converges use LAll goals completed! 🐙 theorem Series.convergesTo_sum {s : Series} (h: s.converges) : s.convergesTo s.sum := bys:Seriesh:s.converges⊢ s.convergesTo s.sum simp [sum, h]s:Seriesh:s.converges⊢ s.convergesTo (Exists.choose ⋯) exact (h.choose_spec)All goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_4a {N:ℤ} (hN: N ≥ 1) : example_7_2_4.partial N = 1 - (2:ℝ)^(-N) := byN:ℤhN:N ≥ 1⊢ example_7_2_4.partial N = 1 - 2 ^ (-N) sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4b : example_7_2_4.convergesTo 1 := by⊢ example_7_2_4.convergesTo 1 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4c : example_7_2_4.sum = 1 := by⊢ example_7_2_4.sum = 1 sorryAll goals completed! 🐙noncomputable abbrev Series.example_7_2_4' := mk' (m := 1) (fun n ↦ (2:ℝ)^(n:ℤ))theorem declaration uses 'sorry'Series.example_7_2_4'a {N:ℤ} (hN: N ≥ 1) : example_7_2_4'.partial N = (2:ℝ)^(N+1) - 2 := byN:ℤhN:N ≥ 1⊢ example_7_2_4'.partial N = 2 ^ (N + 1) - 2 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4'b : example_7_2_4'.diverges := by⊢ example_7_2_4'.diverges sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.diverges_of_nodecay {s:Series} (h: ¬ Filter.Tendsto s.seq Filter.atTop (nhds 0)) : s.diverges := bys:Seriesh:¬Filter.Tendsto s.seq Filter.atTop (nhds 0)⊢ s.diverges sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_7' : ((fun n:ℕ ↦ (-1:ℝ)^n):Series).diverges := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.diverges apply diverges_of_nodecayh⊢ ¬Filter.Tendsto { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.seq Filter.atTop (nhds 0) sorryAll goals completed! 🐙 abbrev Series.absConverges (s:Series) : Prop := s.abs.convergesabbrev Series.condConverges (s:Series) : Prop := s.converges ∧ ¬ s.absConverges theorem declaration uses 'sorry'Series.abs_le {s:Series} (h : s.absConverges) : |s.sum| ≤ s.abs.sum := bys:Seriesh:s.absConverges⊢ |s.sum| ≤ s.abs.sum sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_13a : example_7_2_13.converges := by⊢ example_7_2_13.converges sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13b : ¬ example_7_2_13.absConverges := by⊢ ¬example_7_2_13.absConverges sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13c : example_7_2_13.condConverges := by⊢ example_7_2_13.condConverges sorryAll goals completed! 🐙instance Series.inst_add : Add Series where add a b := { 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 := bya:Seriesb:Series⊢ ∀ 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:Seriesb:Seriesn:ℤ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:Seriesb:Seriesn:ℤ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! 🐙 } instance Series.inst.smul : SMul ℝ Series where smul c s := { m := s.m seq := fun n ↦ if n ≥ s.m then c * s.seq n else 0 vanish := byc:ℝs:Series⊢ ∀ n < s.m, (if n ≥ s.m then c * s.seq n else 0) = 0 intro n hnc:ℝs:Seriesn:ℤhn:n < s.m⊢ (if n ≥ s.m then c * s.seq n else 0) = 0 rw [lt_iff_not_ge] at hnc:ℝs:Seriesn:ℤhn:¬n ≥ s.m⊢ (if n ≥ s.m then c * s.seq n else 0) = 0 simp [hn]All goals completed! 🐙 } abbrev Series.from (s:Series) (m₁:ℤ) : Series := mk' (m := max s.m m₁) (fun n ↦ s.seq (n:ℤ)) theorem declaration uses 'sorry'Series.sum_from {s:Series} (k:ℕ) (h: s.converges) : s.sum = ∑ n ∈ Finset.Ico s.m (s.m+k), s.seq n + (s.from (s.m+k)).sum := bys:Seriesk:ℕh:s.converges⊢ s.sum = ∑ n ∈ Finset.Ico s.m (s.m + ↑k), s.seq n + (s.from (s.m + ↑k)).sum sorryAll goals completed! 🐙 /- Вправа 7.2.1 -/ def declaration uses 'sorry'Series.exercise_7_2_1_convergent : Decidable ( (mk' (m := 1) (fun n ↦ (-1:ℝ)^(n:ℤ))).converges ) := by⊢ Decidable (mk' fun n => (-1) ^ ↑n).converges -- The first line of this proof should be `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙end Chapter7