Enable more linters, fix various lint errors

Changes

2 changed files (+8/-4)

• Sum.lean
  • @@ -14,7 +14,7 @@ lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : ∑ a ∈ Ico
    linarith 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 + 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 ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (n - 1) * (b - 1))) := by
  • @@ -29,9 +29,8 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n): ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    simp norm_num | step h ih => - rw [sum_Ico_succ_top, ih] + rw [sum_Ico_succ_top h, ih] simp - exact h -- Exponentials grow quickly lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by
  • @@ -53,7 +52,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    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] + simp only [this, Nat.ofNat_pos, pow_pos, mul_le_mul_iff_left₀, ge_iff_le] grind · interval_cases n <;> simp
• lakefile.toml
  • @@ -2,6 +2,11 @@ name = "leantest"
    version = "0.1.0" defaultTargets = ["leantest"] + [leanOptions.weak.linter] + mathlibStandardSet = true + flexible = true + style.longLine = false + [[lean_exe]] name = "leantest" root = "Main"