Use ceil instead of floor

Changes

1 changed files (+14/-14)

• sum.lean
  • @@ -117,7 +117,7 @@ lemma exp_larger' (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n -
    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 + use max (Nat.ceil (3 / ε)) 2 intro n nlarge simp have h₁ : n ≥ 2 := by
  • @@ -192,23 +192,23 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    linarith else simp at hε - have h₃ : Nat.floor (3 / ε) ≥ 2 := by - -- have h₄ : 2 ≤ 3 / ε := by - -- rw [mul_le_mul_right.mpr ε] - sorry - have h₄ : n ≥ Nat.floor (3 / ε) := by + have h₃ : n ≥ Nat.ceil (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) := by - if h₈ : n = 2 then - rw [h₈] + have h₄ : 3 / n ≤ ε := by + have h₅ : 3 / ε ≤ n := by + exact Nat.ceil_le.mp h₃ + refine (div_le_comm₀ ?_ εpos).mpr h₅ + norm_num + linarith + have h₅ : 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n := by + 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 + have h₈ : 3 ≤ n := by omega - exact exp_larger' n h₉ + exact exp_larger' n h₈ sorry linarith linarith