#min_imports

Changes

3 changed files (+5/-4)

• Kadane.lean
  • @@ -1,5 +1,5 @@
    import Std.Tactic.Do - import Mathlib + import Mathlib.Analysis.Normed.Ring.Lemmas def kadane (A : Array ℤ) := Id.run do let mut cur := 0
  • @@ -73,5 +73,5 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    · have : j - i = 0 := by grind rw [List.extract, this, List.take_zero] grind [is_max_subarray] - case vc2.a.pre => simp [is_max_nonempty_suffix, is_max_subarray] + case vc2.a.pre => trivial case vc3.a.post => grind
• Sort.lean
  • @@ -1,5 +1,6 @@
    import Std.Tactic.Do - import Mathlib + import Batteries.Data.Array.Pairwise + import Mathlib.Data.Multiset.Defs variable [LinearOrder α] (A : Array α)
• Sum.lean
  • @@ -54,7 +54,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    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 - · interval_cases n <;> decide + · interval_cases n <;> trivial 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)]