grind >>> linarith

Changes

1 changed files (+6/-6)

• Sum.lean
  • @@ -45,7 +45,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    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 + suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by lia have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] simp only [this, Nat.ofNat_pos, pow_pos, mul_le_mul_iff_left₀, ge_iff_le] grind
  • @@ -61,14 +61,14 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    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 + 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 grind 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_cast 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 : ℝ) - 1) ≤ 1 := div_le_one₀ (by lia) |>.mpr (by lia) have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by simp_rw [one_div] exact inv_anti₀ (by norm_num) <| pow_le_pow_left₀ (by norm_num) h₃ (n - 1)
  • @@ -79,8 +79,8 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    norm_cast · 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 + have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by lia) |>.mpr (by lia) + suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by grind have := exp_larger n h₁ rw [← one_mul (2 ^ (n - 1))] at this exact div_le_div_iff₀ (by norm_num) (by norm_num) |>.mpr (by norm_cast)
  • @@ -100,6 +100,6 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    have h₂ b (bico : b ∈ Ico 2 n) : 0 ≤ (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by rw [one_div_nonneg] have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) - exact mul_nonneg (pow_nonneg (by linarith) (n - 1)) (by linarith) + exact mul_nonneg (pow_nonneg (by lia) (n - 1)) (by lia) have : 0 < (1 : ℝ) / (n - 1) := by simp [Nat.one_lt_cast.mpr h₁] grind [sum_nonneg h₂]