OK almost done with the proof

Changes

1 changed files (+74/-35)

• sum.lean
  • @@ -11,12 +11,14 @@ example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = n ^ 2 := by
    induction n with | zero => trivial | succ n ih => - -- have blah (k : ℕ) : 2 * k + 1 = 2 * (k + 1) - 1 := by sorry - -- rw [blah] rw [sum_range_succ, ih] ring - -- example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * k + 1)) := by + -- How to rw the inside of a sum + example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * (k + 1) - 1)) := by + apply Finset.sum_congr rfl + intro k hk + omega def converges_to (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
  • @@ -43,39 +45,76 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ a ∈
    linarith simp [h₄, div_mul_cancel_left₀ h₃] + lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by + calc + ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 N, ∑ a ∈ Ico 2 N, (1 : ℝ) / (b ^ a) := sum_comm + _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1))) := by + apply Finset.sum_congr rfl + intro b bico + have h₁ : (b : ℝ) ≥ 2 := by + have h₂ : b ≥ 2 := List.left_le_of_mem_range' bico + exact Nat.ofNat_le_cast.mpr h₂ + exact geom_sum b N h h₁ + _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := sum_sub_distrib + _ = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by + have h₁ : ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) := by + induction h with + | refl => + field_simp + linarith + | step h ih => + rw [sum_Ico_succ_top, ih] + field_simp + exact h + rw [h₁] + lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by intro ε εpos - use max (Nat.floor (1 / ε)) 2 - intro n nlarge + use max (Nat.floor (2 / ε)) 2 + intro N Nlarge simp - have h₁ : n ≥ 2 := by - exact le_of_max_le_right nlarge - have h₂ (b : ℕ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ∈ Ico 2 N) : ∑ a ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = (1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by - have h₃ : (b : ℝ) ≥ 2 := by - have h₄ : b ≥ 2 := List.left_le_of_mem_range' h₂ - exact Nat.ofNat_le_cast.mpr h₄ - exact geom_sum ↑b N h₁ h₃ - have h₃ : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by - calc - ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm - _ = ∑ b ∈ Ico 2 n, (1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1))) := by - rw [h₂ _ n h₁] - - - _ = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by - induction n with - | zero => trivial - | succ n ih => - cases h₁ - field_simp - rename_i h₃ - push_cast - push_cast at ih - rw [sum_Ico_succ_top, ih _ h₃] - - - -- rw [h₂] - + have h₁ : N ≥ 2 := by + exact le_of_max_le_right Nlarge + rw [abs_lt] + constructor + -- Greater than 1 - ε + field_simp + rw [telescope_sum N h₁] + ring_nf - -- then telescope the sums and bound the other sum - -- qed + -- have h₂ : -ε < ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) - 1 := by + -- rw [telescope_sum N h₁] + -- sorry + -- simp + -- simp at h₂ + -- exact h₂ + sorry + -- Less than 1 + field_simp + rw [telescope_sum N h₁] + ring_nf + field_simp + have h₂ : (1 : ℝ) / (-1 + N) > 0 := by + field_simp + linarith + have h₃ : ∀ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) > 0 := by + intro b bico + field_simp + have h₄ : b ≥ 2 := List.left_le_of_mem_range' bico + have h₅ : (b : ℝ) > 1 := Nat.one_lt_cast.mpr h₄ + have h₆ : (b : ℝ) ^ (N - 1) > 0 := by + have h₇ : (b : ℝ) > 0 := by linarith + apply pow_pos h₇ + have h₇ : (b : ℝ) - 1 > 0 := by + linarith + apply mul_pos h₆ h₇ + have h₄ : ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) ≥ 0 := by + have h₅ : ∀ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) ≥ 0 := by + exact fun b a => le_of_lt (h₃ b a) + exact sum_nonneg h₅ + ring_nf at h₄ + field_simp at h₄ + have h₅ : -(1 : ℝ) / (-1 + N) < 0 := by + nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc] + linarith + linarith