Almost done with double sum proof

Changes

1 changed files (+73/-91)

• sum.lean
  • @@ -1,62 +1,10 @@
    import Mathlib open Finset BigOperators - example (n b : ℕ) (h₁ : n ≥ 2) (h₂ : b ≥ 2) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by - have h_b_sub_one : (b : ℝ) - 1 ≥ 1 := by - have h₃ : (b : ℝ) ≥ 2 := by exact_mod_cast h₂ - linarith - - have h_b_pow : (b : ℝ) ^ (n - 1) ≥ 2 ^ (n - 1) := by - have h₃ : (b : ℝ) ≥ 2 := by exact_mod_cast h₂ - have h₄ : (n - 1 : ℕ) ≥ 1 := by - have h₅ : n ≥ 2 := h₁ - have h₆ : n - 1 ≥ 1 := by - omega - exact h₆ - have h₅ : (b : ℝ) ^ (n - 1) ≥ 2 ^ (n - 1) := by - exact pow_le_pow_iff_left₀ (by linarith) h₃ (by linarith) - exact h₅ - - have h_main : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) ≥ 2 ^ (n - 1) := by - have h₃ : (b : ℝ) ^ (n - 1) ≥ 2 ^ (n - 1) := h_b_pow - have h₄ : (b : ℝ) - 1 ≥ 1 := h_b_sub_one - have h₅ : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) ≥ 2 ^ (n - 1) * 1 := by - calc - (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) ≥ 2 ^ (n - 1) * ((b : ℝ) - 1) := by - exact mul_le_mul_of_nonneg_right h₃ (by linarith) - _ ≥ 2 ^ (n - 1) * 1 := by - have h₆ : (b : ℝ) - 1 ≥ 1 := h_b_sub_one - have h₇ : (2 : ℝ) ^ (n - 1) ≥ 0 := by positivity - nlinarith - nlinarith - - have h_final : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by - have h₃ : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) ≥ 2 ^ (n - 1) := h_main - have h₄ : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) > 0 := by - have h₅ : (b : ℝ) ≥ 2 := by exact_mod_cast h₂ - have h₆ : (b : ℝ) - 1 ≥ 1 := h_b_sub_one - have h₇ : (b : ℝ) ^ (n - 1) ≥ 2 ^ (n - 1) := h_b_pow - have h₈ : (b : ℝ) ^ (n - 1) > 0 := by positivity - have h₉ : (b : ℝ) - 1 > 0 := by linarith - positivity - have h₅ : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by - -- Use the fact that the denominator on the left is larger to prove the inequality - have h₆ : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) ≥ 2 ^ (n - 1) := h_main - have h₇ : (b : ℝ) ^ (n - 1) * ((b : ℝ) - 1) > 0 := h₄ - have h₈ : (2 : ℝ) ^ (n - 1) > 0 := by positivity - -- Use the division inequality to prove the result - have h₉ : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by - apply (div_le_div_iff₀ (by positivity) (by positivity)).mpr - nlinarith - exact h₉ - exact h₅ - - exact h_final - - -- OK let's do some warm-up example (b : ℝ) (h : b ≥ 2) : 1 / ((b - 1) * b) = 1 / (b - 1) - 1 / b := by - have h₁ : b - 1 ≠ 0 := by linarith + have h₁ : b - 1 ≠ 0 := by + linarith field_simp -- More easy stuff
  • @@ -73,6 +21,7 @@ example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.
    intro k hk omega + -- Pretty standard epsilon delta thing def converges_to (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
  • @@ -80,7 +29,8 @@ def converges_to (s : ℕ → ℝ) (a : ℝ) :=
    -- This was so excruciating wow lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ 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'] by_contra h
  • @@ -88,11 +38,13 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ a ∈
    linarith exact h₁ _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by - have h₃ : b - 1 ≠ 0 := by linarith + have h₃ : 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
  • @@ -104,9 +56,7 @@ lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1))) := by apply Finset.sum_congr rfl intro b bico - have h₁ : (b : ℝ) ≥ 2 := by - have h₂ : b ≥ 2 := List.left_le_of_mem_range' bico - exact Nat.ofNat_le_cast.mpr h₂ + have h₁ : (b : ℝ) ≥ 2 := 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)) := sum_sub_distrib _ = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by
  • @@ -121,9 +71,35 @@ lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    exact h rw [h₁] + -- Exponentials grow quickly + lemma exp_larger (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := by + have h₁ : n * (n - 1) < 2 ^ n := by + induction h with + | refl => + trivial + | step a a_ih => + rename_i m + simp + simp at a + have h₂ : (m + 1) * m ≤ 2 * (m * (m - 1)) := by + nth_rw 3 [mul_comm] + rw [←mul_assoc] + apply Nat.mul_le_mul_right m + omega + have h₃ : 2 * 2 ^ m = 2 ^ (m + 1) := Eq.symm Nat.pow_succ' + linarith + have h₂ : 2 ^ n ≤ (3 * n - 4) * 2 ^ (n - 1) := by + have h₃ : 2 ^ n = 2 * 2 ^ (n - 1) := by + apply Eq.symm (mul_pow_sub_one ?_ 2) + linarith + rw [h₃] + apply Nat.mul_le_mul_right (2 ^ (n - 1)) + omega + linarith + lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by intro ε εpos - use max (Nat.floor (2 / ε)) 2 + use max (Nat.floor (4 / ε)) 2 intro n nlarge simp have h₁ : n ≥ 2 := by
  • @@ -138,41 +114,47 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    have h₃ : ∀ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by intro b bico have h₄ : b ≥ 2 := List.left_le_of_mem_range' bico - have h₅ : (b : ℝ) > 0 := by + have h₅ : 1 / ((b : ℝ) - 1) ≤ 1 := by + have h₀ : (b : ℝ) - 1 > 0 := by + simp + linarith + field_simp sorry - have h₆ : (b : ℝ) - 1 ≠ 0 := by + have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by sorry - have h₇ : ((b : ℝ) ^ (n - 1) * ((b : ℝ) - 1)) ≠ 0 := by + have h₇ : 0 ≤ 1 / (b : ℝ) ^ (n - 1) := by sorry - field_simp - - have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ ∑ b ∈ Ico 2 n, 1 / 2 ^ (n - 1) := by - exact sum_le_sum h₃ + have h₈ : (0 : ℝ) ≤ 1 := by + norm_num + rw [←one_div_mul_one_div, mul_comm] + nth_rw 5 [←one_mul 1] + rw [mul_div_assoc] + exact mul_le_mul h₅ h₆ h₇ h₈ + have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ ∑ b ∈ Ico 2 n, 1 / 2 ^ (n - 1) := sum_le_sum h₃ field_simp at h₄ field_simp exact h₄ ring_nf at h₂ - rel [h₂] - - - -- if h₂ : ε ≥ 1 then - -- have h₃ : Nat.floor (2 / ε) ≤ 2 := by - -- linarith - -- have h₃ : max (Nat.floor (2 / ε)) 2 = 2 := by - -- exact Nat.max_eq_right h₃ - -- rw [h₃] at nlarge - - - -- else + have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by + have h₄ : 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε := by + if hε : ε > 1 then - - - -- rw [telescope_sum N h₁] - -- sorry - -- simp - -- simp at h₂ - -- exact h₂ - sorry + sorry + else + simp at hε + have h₃ : Nat.floor (4 / ε) ≥ 2 := by + sorry + have h₄ : n ≥ Nat.floor (4 / ε) := by + exact le_of_max_le_left nlarge + have h₅ : ε ≥ 3 / n := by + sorry + have h₆ : 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / (n : ℝ) := by + have h₇ : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := exp_larger n h₁ + sorry + linarith + linarith + ring_nf at h₃ + linarith -- Less than 1 field_simp rw [telescope_sum n h₁]
  • @@ -187,14 +169,14 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    have h₄ : b ≥ 2 := List.left_le_of_mem_range' bico have h₅ : (b : ℝ) > 1 := Nat.one_lt_cast.mpr h₄ have h₆ : (b : ℝ) ^ (n - 1) > 0 := by - have h₇ : (b : ℝ) > 0 := by linarith + have h₇ : (b : ℝ) > 0 := by + linarith apply pow_pos h₇ have h₇ : (b : ℝ) - 1 > 0 := by linarith apply mul_pos h₆ h₇ have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≥ 0 := by - have h₅ : ∀ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≥ 0 := by - exact fun b a => le_of_lt (h₃ b a) + have h₅ : ∀ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≥ 0 := fun b a => le_of_lt (h₃ b a) exact sum_nonneg h₅ ring_nf at h₄ field_simp at h₄