Nearly nearly done

Changes

1 changed files (+40/-4)

• sum.lean
  • @@ -72,7 +72,25 @@ lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    rw [h₁] -- Exponentials grow quickly - lemma exp_larger (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := by + lemma exp_larger (n : ℕ) (h : n ≥ 3) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by + induction h with + | refl => + trivial + | step a a_ih => + rename_i m + simp + simp at a + have h₁ : 2 * 2 ^ (m - 1) = 2 ^ m := by + apply mul_pow_sub_one + linarith + rw [←h₁] + apply Nat.mul_le_mul_left 2 + have h₂ : m - 1 ≤ 2 * (m - 2) := by + omega + linarith + + -- Another similar lemma + lemma exp_larger' (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := by have h₁ : n * (n - 1) < 2 ^ n := by induction h with | refl =>
  • @@ -97,7 +115,7 @@ lemma exp_larger (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n -
    omega linarith - lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by + theorem 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 (3 / ε)) 2 intro n nlarge
  • @@ -146,7 +164,25 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by have h₄ : 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε := by if hε : ε > 3 / 2 then - sorry + have h₅ : (n : ℝ) ≥ 2 := by + norm_num + linarith + have h₆ : 1 / ((n : ℝ) - 1) ≤ 1 := by + have h₇ : (n : ℝ) - 1 ≥ 1 := by + linarith + refine (div_le_one₀ ?_).mpr h₇ + linarith + have h₇ : ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 := by + have h₈ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by + if h₉ : n = 2 then + rw [h₉] + norm_num + else + have h₁₀ : 3 ≤ n := by + omega + exact exp_larger n h₁₀ + sorry + linarith else simp at hε have h₃ : Nat.floor (3 / ε) ≥ 2 := by
  • @@ -165,7 +201,7 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    else have h₉ : 3 ≤ n := by omega - exact exp_larger n h₉ + exact exp_larger' n h₉ sorry linarith linarith