Use mathlib convention of putting one-liner proofs on the same line

Changes

1 changed files (+11/-25)

• Sum.lean
  • @@ -2,26 +2,22 @@ import Mathlib
    open Finset BigOperators -- Pretty standard epsilon delta thing - def converges_to (s : ℕ → ℝ) (a : ℝ) := - ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε + def converges_to (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 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)) := calc - ∑ a ∈ Ico 2 N, 1 / (b ^ a) = ∑ a ∈ Ico 2 N, (1 / b) ^ a := by - simp + ∑ 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'] grind exact h₁ _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by - have : b - 1 ≠ 0 := by - linarith + 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 ≠ 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
  • @@ -35,8 +31,7 @@ lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    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₁ - _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by - apply sum_sub_distrib + _ = ∑ 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] induction h with
  • @@ -78,10 +73,7 @@ lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3)
    apply Nat.mul_le_mul_right (m * (m - 1)) omega suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith - have h₂ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by - rw [mul_pow_sub_one] - omega - omega + have h₂ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by grind [mul_pow_sub_one] rw [h₂, ←mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega
  • @@ -158,11 +150,8 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    exact exp_larger' n (by omega) apply lt_sub_iff_add_lt'.mp have h₅ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by - have : (n : ℝ) ≠ 0 := by - rw [Nat.cast_ne_zero] - omega - have : (n : ℝ) - 1 ≠ 0 := by - grind + have : (n : ℝ) ≠ 0 := by grind [Nat.cast_ne_zero] + have : (n : ℝ) - 1 ≠ 0 := by grind field_simp ring rw [h₅]
  • @@ -175,11 +164,9 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₈ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] simp - have h₉ : ↑(n - 2) = (n : ℝ) - 2 := by - norm_cast + have h₉ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast rwa [h₇, h₈, h₉] at h₄ - have h₇ : 0 < (2 : ℝ) ^ (n - 1) := by - norm_num + have h₇ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact (div_lt_div_iff₀ h₇ (by nlinarith)).mpr h₆ ring_nf at h₃ linarith
  • @@ -195,8 +182,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    intro b bico field_simp have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) - have h₃ : 0 < (b : ℝ) ^ (n - 1) := by - apply pow_pos (by linarith) + have h₃ : 0 < (b : ℝ) ^ (n - 1) := by apply pow_pos (by linarith) exact mul_pos h₃ (by linarith) have h₃ : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := sum_nonneg (fun b a => le_of_lt (h₂ b a)) field_simp at h₃