Try to avoid non-terminal simps https://lean-lang.org/doc/reference/latest/The-Simplifier/Terminal-vs-Non-Terminal-Positions/

Changes

1 changed files (+4/-4)

• Sum.lean
  • @@ -9,11 +9,10 @@ lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : ∑ a ∈ Ico
    have : ∑ a ∈ Ico 2 n, 1 / (b ^ a) = ∑ a ∈ Ico 2 n, (1 / b) ^ a := by simp rw [this, geom_sum_Ico' (by grind) hn] field_simp - simp have : b ^ n ≠ 0 := by have : 0 < b ^ n := pow_pos (by linarith) n linarith - grind [mul_pow_sub_one] + grind [one_div, inv_pow, mul_pow_sub_one] 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
  • @@ -61,11 +60,12 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)] intro ε εpos - simp + simp only [true_and, Set.mem_Ici, Set.mem_Ioo] use max (Nat.ceil (3 / ε)) 2 intro n nlarge have h₁ := le_of_max_le_right nlarge - constructor <;> field_simp <;> rw [telescope_sum n h₁] + rw [telescope_sum n h₁] + constructor · -- Greater than 1 - ε 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