Don't need ring_nf, slightly reorganize proof

Changes

1 changed files (+9/-16)

• Sum.lean
  • @@ -65,29 +65,25 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    use max (Nat.ceil (3 / ε)) 2 intro n nlarge have h₁ : 2 ≤ n := le_of_max_le_right nlarge - constructor <;> field_simp <;> rw [telescope_sum n h₁] <;> ring_nf + constructor <;> field_simp <;> rw [telescope_sum n h₁] · -- Greater than 1 - ε - have : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1) := by - have h₂ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by + suffices (∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1)) ∧ 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith + constructor + · have h₂ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by rw [← one_div_mul_one_div] have h₃ : 2 ≤ (b : ℝ) := by norm_num exact (List.left_le_of_mem_range' bico) have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := (div_le_one₀ (by linarith)).mpr (by linarith) have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by - simp only [← one_div_pow] - apply pow_le_pow_left₀ (by norm_num) - simp - exact inv_anti₀ (by norm_num) h₃ + simp only [one_div] + exact inv_anti₀ (by norm_num) (pow_le_pow_left₀ (by norm_num) h₃ (n - 1)) grw [h₄, h₅] simp grw [sum_le_sum h₂] simp norm_cast - ring_nf at this - have : 0 < ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by - suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith - by_cases hε : 3 / 2 < ε + · by_cases 3 / 2 < ε · have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith
  • @@ -96,19 +92,16 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) · have : 3 / n ≤ ε := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) grw [← this] - rw [← lt_sub_iff_add_lt'] have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by field_simp grind - rw [this] + rw [← lt_sub_iff_add_lt', this] have h₂ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by have := exp_larger' n h₁ - rify [h₁] at this + rify at this grind [Nat.cast_sub] have h₃ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact (div_lt_div_iff₀ h₃ (by nlinarith)).mpr h₂ - ring_nf at this - linarith · -- Less than 1 have h₂ b (bico : b ∈ Ico 2 n) : 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by rw [one_div_pos]