Don't name so many hypotheses in Sum.lean

Changes

1 changed files (+34/-38)

• Sum.lean
  • @@ -2,21 +2,21 @@ import Mathlib
    open Finset BigOperators Filter Topology -- Important: b should be in ℝ so that it's real div not nat div - lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : 2 ≤ N) (h₂ : 2 ≤ b) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := + lemma geom_sum (N : ℕ) (b : ℝ) (hN : 2 ≤ N) (hb : 2 ≤ b) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := calc ∑ a ∈ Ico 2 N, 1 / (b ^ a) = ∑ a ∈ Ico 2 N, (1 / b) ^ a := by simp _ = ((1 / b) ^ 2 - (1 / b) ^ N) / (1 - (1 / b)) := by - rw [geom_sum_Ico' (by grind) h₁] + rw [geom_sum_Ico' (by grind) hN] _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by have : b - 1 ≠ 0 := by linarith field_simp ring _ = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := by - have h₃ : b ≠ 0 := by linarith - have h₄ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by + 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] linarith - simp [h₄, div_mul_cancel_left₀ h₃] + simp [h₂, div_mul_cancel_left₀ h₁] lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by calc
  • @@ -24,8 +24,7 @@ lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1))) := by apply Finset.sum_congr rfl intro b bico - have h₁ : 2 ≤ (b : ℝ) := Nat.ofNat_le_cast.mpr (List.left_le_of_mem_range' bico) - exact geom_sum b N h h₁ + exact geom_sum N b h <| Nat.ofNat_le_cast.mpr (List.left_le_of_mem_range' bico) _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by apply sum_sub_distrib _ = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by suffices ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) by rw [this]
  • @@ -63,8 +62,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    · 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 - rw [this.tendsto_iff (nhds_basis_Ioo_pos 1)] + rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)] intro ε εpos simp use max (Nat.ceil (3 / ε)) 2
  • @@ -72,67 +70,65 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    have h₁ : 2 ≤ n := le_of_max_le_right nlarge constructor <;> field_simp <;> rw [telescope_sum n h₁] <;> ring_nf · -- Greater than 1 - ε - have h₂ : ∑ 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 - have h₄ : 2 ≤ (b : ℝ) := by + 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 + 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 - rw [← one_div_pow, ← one_div_pow] + 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₄ + exact inv_anti₀ (by norm_num) h₃ rw [← one_div_mul_one_div, mul_comm] nth_rw 5 [← one_mul 1] rw [mul_div_assoc] - exact mul_le_mul h₅ h₆ (by norm_num) (by norm_num) - 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₄ + exact mul_le_mul h₄ h₅ (by norm_num) (by norm_num) + have := sum_le_sum h₂ field_simp - exact h₄ - ring_nf at h₂ - have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by + field_simp at this + exact this + ring_nf at this + have : 1 < 1 + ε - 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 < ε · 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₄ := exp_larger n h₁ - rw [mul_comm, ← one_mul (2 ^ (n - 1))] at h₄ + have := exp_larger n h₁ + rw [mul_comm, ← one_mul (2 ^ (n - 1))] at this exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) · simp at hε have : 3 / n ≤ ε := by - have h₃ : 3 / ε ≤ n := Nat.ceil_le.mp (le_of_max_le_left nlarge) - have h₄ : 0 < (n : ℝ) := by + have : 0 < (n : ℝ) := by norm_num omega - exact (div_le_comm₀ h₄ εpos).mpr h₃ + exact (div_le_comm₀ this εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) suffices 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n by linarith rw [← lt_sub_iff_add_lt'] - have h₃ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by - have : (n : ℝ) ≠ 0 := by grind [Nat.cast_ne_zero] + have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by have : (n : ℝ) - 1 ≠ 0 := by grind field_simp ring - rw [h₃] - have h₄ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by - have h₅ := exp_larger' n h₁ - have h₆ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by + rw [this] + have h₂ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by + have h₃ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] simp - rify [h₁, h₆] at h₅ + have := exp_larger' n h₁ + rify [h₁, h₃] 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 h₃ + 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 field_simp have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) exact mul_pos (pow_pos (by linarith) (n - 1)) (by linarith) - have : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := sum_nonneg (fun b a => le_of_lt (h₂ b a)) + have := sum_nonneg (fun b a => le_of_lt (h₂ b a)) have : 0 < (1 : ℝ) / (n - 1) := by field_simp omega