Nearly done with proof

Changes

1 changed files (+38/-22)

• sum.lean
  • @@ -46,7 +46,7 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ a ∈
    have h₃ : b ≠ 0 := by linarith have h₄ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by - rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one] + rw [←mul_assoc, ←pow_succ' b (N - 1), Nat.sub_one_add_one] linarith simp [h₄, div_mul_cancel_left₀ h₃]
  • @@ -86,20 +86,20 @@ lemma exp_larger (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n -
    rw [←mul_assoc] apply Nat.mul_le_mul_right m omega - have h₃ : 2 * 2 ^ m = 2 ^ (m + 1) := Eq.symm Nat.pow_succ' + have h₃ : 2 ^ (m + 1) = 2 * 2 ^ m := Nat.pow_succ' linarith have h₂ : 2 ^ n ≤ (3 * n - 4) * 2 ^ (n - 1) := by - have h₃ : 2 ^ n = 2 * 2 ^ (n - 1) := by - apply Eq.symm (mul_pow_sub_one ?_ 2) + have h₃ : 2 * 2 ^ (n - 1) = 2 ^ n := by + apply mul_pow_sub_one linarith - rw [h₃] + rw [←h₃] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega linarith 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 (4 / ε)) 2 + use max (Nat.floor (3 / ε)) 2 intro n nlarge simp have h₁ : n ≥ 2 := by
  • @@ -114,22 +114,30 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    have h₃ : ∀ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by intro b bico have h₄ : b ≥ 2 := List.left_le_of_mem_range' bico - have h₅ : 1 / ((b : ℝ) - 1) ≤ 1 := by - have h₀ : (b : ℝ) - 1 > 0 := by - simp + have h₅ : (b : ℝ) ≥ 2 := by + norm_num + linarith + have h₆ : 1 / ((b : ℝ) - 1) ≤ 1 := by + have h₇ : (b : ℝ) - 1 ≥ 1 := by linarith - field_simp - sorry - have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by - sorry - have h₇ : 0 ≤ 1 / (b : ℝ) ^ (n - 1) := by - sorry - have h₈ : (0 : ℝ) ≤ 1 := by + refine (div_le_one₀ ?_).mpr h₇ + linarith + have h₇ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by + rw [←one_div_pow, ←one_div_pow] + apply pow_le_pow_left₀ + norm_num + simp + apply inv_anti₀ at h₅ + exact h₅ + norm_num + have h₈ : 0 ≤ 1 / (b : ℝ) ^ (n - 1) := by + norm_num + have h₉ : (0 : ℝ) ≤ 1 := by norm_num rw [←one_div_mul_one_div, mul_comm] nth_rw 5 [←one_mul 1] rw [mul_div_assoc] - exact mul_le_mul h₅ h₆ h₇ h₈ + exact mul_le_mul h₆ h₇ h₈ h₉ have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ ∑ b ∈ Ico 2 n, 1 / 2 ^ (n - 1) := sum_le_sum h₃ field_simp at h₄ field_simp
  • @@ -137,19 +145,27 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    ring_nf at h₂ 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ε : ε > 1 then - + if hε : ε > 3 / 2 then sorry else simp at hε - have h₃ : Nat.floor (4 / ε) ≥ 2 := by + have h₃ : Nat.floor (3 / ε) ≥ 2 := by + -- have h₄ : 2 ≤ 3 / ε := by + -- rw [mul_le_mul_right.mpr ε] sorry - have h₄ : n ≥ Nat.floor (4 / ε) := by + have h₄ : n ≥ Nat.floor (3 / ε) := by exact le_of_max_le_left nlarge have h₅ : ε ≥ 3 / n := by sorry have h₆ : 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / (n : ℝ) := by - have h₇ : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := exp_larger n h₁ + have h₇ : n * (n - 1) < (3 * n - 4) * 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 linarith