A bit more progress

Changes

1 changed files (+96/-12)

• sum.lean
  • @@ -1,6 +1,59 @@
    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
  • @@ -71,18 +124,49 @@ lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    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 - intro N Nlarge + intro n nlarge simp - have h₁ : N ≥ 2 := by - exact le_of_max_le_right Nlarge + have h₁ : n ≥ 2 := by + exact le_of_max_le_right nlarge rw [abs_lt] constructor -- Greater than 1 - ε field_simp - rw [telescope_sum N h₁] + rw [telescope_sum n h₁] ring_nf + have h₂ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1) := by + 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 + sorry + have h₆ : (b : ℝ) - 1 ≠ 0 := by + sorry + have h₇ : ((b : ℝ) ^ (n - 1) * ((b : ℝ) - 1)) ≠ 0 := 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₃ + 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₂ : -ε < ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) - 1 := by -- rw [telescope_sum N h₁] -- sorry -- simp
  • @@ -91,30 +175,30 @@ lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico
    sorry -- Less than 1 field_simp - rw [telescope_sum N h₁] + rw [telescope_sum n h₁] ring_nf field_simp - have h₂ : (1 : ℝ) / (-1 + N) > 0 := by + have h₂ : (1 : ℝ) / (-1 + n) > 0 := by field_simp linarith - 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 intro b bico field_simp 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 : ℝ) ^ (n - 1) > 0 := by 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 + 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) exact sum_nonneg h₅ ring_nf at h₄ field_simp at h₄ - have h₅ : -(1 : ℝ) / (-1 + N) < 0 := by + have h₅ : -(1 : ℝ) / (-1 + n) < 0 := by nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc] linarith linarith