Simplify Sum.lean even more using grind, positivity, grw

Changes

4 changed files (+25/-36)

• Sum.lean
  • @@ -69,6 +69,7 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    · -- Greater than 1 - ε have : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1) := by 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_num exact (List.left_le_of_mem_range' bico)
  • @@ -78,16 +79,13 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    apply pow_le_pow_left₀ (by norm_num) simp exact inv_anti₀ (by norm_num) h₃ - rw [← one_div_mul_one_div, mul_comm] - nth_rw 5 [← one_mul 1] - rw [mul_div_assoc] - exact mul_le_mul h₄ h₅ (by norm_num) (by norm_num) - have := sum_le_sum h₂ + grw [h₄, h₅] + simp + grw [sum_le_sum h₂] simp - simp [Nat.cast_sub h₁] at this - exact this + norm_cast ring_nf at this - have : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by + have : 0 < ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith by_cases hε : 3 / 2 < ε · have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁
  • @@ -96,25 +94,16 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    have := exp_larger n h₁ rw [mul_comm, ← one_mul (2 ^ (n - 1))] at this exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) - · simp at hε - have : 3 / n ≤ ε := by - have : 0 < (n : ℝ) := by - norm_num - omega - exact (div_le_comm₀ this εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) - suffices 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n by linarith + · have : 3 / n ≤ ε := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) + grw [← this] rw [← lt_sub_iff_add_lt'] have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by - have : (n : ℝ) - 1 ≠ 0 := by grind field_simp - ring + grind rw [this] have h₂ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by - have h₃ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by - rw [Nat.cast_sub (by linarith)] - simp have := exp_larger' n h₁ - rify [h₁, h₃] at this + rify [h₁] at this grind [Nat.cast_sub] have h₃ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact (div_lt_div_iff₀ h₃ (by nlinarith)).mpr h₂
• lake-manifest.json
  • @@ -5,17 +5,17 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "37df177aaa770670452312393d4e84aaad56e7b6", + "rev": "eed770a434957369c6262aa3fb1d6426419016d4", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.23.0", + "inputRev": "v4.24.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9", + "rev": "c205f530395b57b520d3d78d975293f0c69b65ce", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -35,37 +35,37 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957", + "rev": "a564b9c2252afef6e0d40613d4ec086b54ffe7df", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "rev": "557f2069977de1c95e68de09e693bc4d1eee7842", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.71", + "inputRev": "v0.0.72-pre", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "247ff80701c76760523b5d7c180b27b7708faf38", + "rev": "fc97e592e3e150370f17a12e3613e96252c4d3d0", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65", + "rev": "345a958916d27982d4ecb4500fba0ebb21096651", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,17 +75,17 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d117e2c28cba42e974bc22568ac999492a34e812", + "rev": "b3a8bc5f8b72102ebbe4da3302432b196e215522", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc", + "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
• lakefile.toml
  • @@ -13,4 +13,4 @@ root = "Gcd"
    [[require]] name = "mathlib" scope = "leanprover-community" - rev = "v4.23.0" + rev = "v4.24.0-rc1"
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.23.0 + leanprover/lean4:v4.24.0-rc1