Move some stuff from the theorem into the exp_larger lemmas

Changes

1 changed files (+22/-28)

• Sum.lean
  • @@ -39,28 +39,28 @@ lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    exact h -- Exponentials grow quickly - lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by - induction h with - | refl => - trivial - | step h ih => - grind [mul_pow_sub_one] + lemma exp_larger (n : ℕ) (h : 2 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by + by_cases h : 2 < n + · induction h + · trivial + · grind [mul_pow_sub_one] + · grind -- Another similar lemma - lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by - have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by - induction h with - | refl => - trivial - | step h ih => - rename_i m - suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind - apply Nat.mul_le_mul_right (m * (m - 1)) - grind - suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith - have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] - simp [this] - omega + lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by + by_cases h : 4 < n + · have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by + induction h + · trivial + · rename_i m _ _ + suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind + apply Nat.mul_le_mul_right (m * (m - 1)) + grind + suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith + have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] + simp [this] + omega + · interval_cases n <;> simp theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by have : atTop.HasBasis (fun _ : ℕ ↦ True) Set.Ici := atTop_basis
  • @@ -98,10 +98,7 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 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 - have h₄ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by - by_cases h₅ : n > 2 - · exact exp_larger n h₅ - · grind + have h₄ := exp_larger n h₁ rw [mul_comm, ← one_mul (2 ^ (n - 1))] at h₄ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) · simp at hε
  • @@ -120,10 +117,7 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    ring rw [h₃] have h₄ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by - have h₅ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by - by_cases h₆ : n > 4 - · exact exp_larger' n h₆ - · interval_cases n <;> simp + have h₅ := exp_larger' n h₁ nth_rw 1 [mul_comm] at h₅ rify at h₅ have h₆ : ↑(n - 1) = (n : ℝ) - 1 := by grind [Nat.cast_sub]