/sum.lean at 8bc73dd3de3995f595c02627780404d8133a8cba

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
  field_simp

-- More easy stuff
example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = n ^ 2 := by
  induction n with
  | zero => trivial
  | succ n ih =>
    rw [sum_range_succ, ih]
    ring

-- How to rw the inside of a sum
example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * (k + 1) - 1)) := by
  apply Finset.sum_congr rfl
  intro k hk
  omega

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

-- Important: b should be in ℝ so that it's real div not nat div
-- 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
    _ = ((1 / b) ^ 2 - (1 / b) ^ N) / (1 - (1 / b)) := by
      rw [geom_sum_Ico']
      by_contra h
      simp at h
      linarith
      exact h₁
    _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by
      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 ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by
        rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one]
        linarith
      simp [h₄, div_mul_cancel_left₀ h₃]

lemma telescope_sum (N : ℕ) (h : N ≥ 2): ∑ 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
      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₂
      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
      have h₁ : ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) := by
        induction h with
        | refl =>
          field_simp
          linarith
        | step h ih =>
          rw [sum_Ico_succ_top, ih]
          field_simp
          exact h
      rw [h₁]

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
  simp
  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₁]
  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



    -- rw [telescope_sum N h₁]
    -- sorry
  -- simp
  -- simp at h₂
  -- exact h₂
  sorry
  -- Less than 1
  field_simp
  rw [telescope_sum n h₁]
  ring_nf
  field_simp
  have h₂ : (1 : ℝ) / (-1 + n) > 0 := by
    field_simp
    linarith
  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 : ℝ) > 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)
    exact sum_nonneg h₅
  ring_nf at h₄
  field_simp at h₄
  have h₅ : -(1 : ℝ) / (-1 + n) < 0 := by
    nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc]
    linarith
  linarith