quick proof that the harmonic series diverges

Stream: new members

[Rado Kirov]

quick lean challenge - can someone write this proof in Lean using mathlib:

image.png
https://x.com/PhDPersuasion/status/1989444431725076728

[Jireh Loreaux]

I'm laying in bed, and I'm not going to get up to do it, but the key lemma is docs#tsum_even_add_odd

[Weiyi Wang]

Using tsum would only show that this doesn't converge absolutely, but the intent is to also show that this doesn't even converge conditionally, right?

[Scott Carnahan]

I suppose we should have a lemma asserting the equivalence of absolute and conditional convergence for totally non-negative functions.

[Kenny Lau]

alternatively, we can work in ENNReal

[Jireh Loreaux]

@Rado Kirov Here's a faithful translation of that argument (if you're willing to accept unconditional convergence, otherwise you'll need to prove that unconditional convergence and conditional convergence coincide for nonnegative functions):

import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Order
import Mathlib.Topology.Algebra.InfiniteSum.Ring

example : ¬ Summable (fun n : ℕ ↦ (n + 1 : ℝ)⁻¹) := by
  intro h
  have hₑ : Summable ((fun n : ℕ ↦ (n + 1 : ℝ)⁻¹) ∘ (2 * ·)) :=
    h.comp_injective fun _ ↦ by grind
  have hₒ : Summable ((fun n : ℕ ↦ (n + 1 : ℝ)⁻¹) ∘ (2 * · + 1)) :=
    h.comp_injective fun _ ↦ by grind
  simp only [Function.comp_def] at hₑ hₒ
  have := calc
    ∑' n : ℕ, (n + 1 : ℝ)⁻¹
    _ = ∑' n : ℕ, ((2 * n : ℕ) + 1 : ℝ)⁻¹ + ∑' n : ℕ, ((2 * n + 1 : ℕ) + 1 : ℝ)⁻¹ := by
      rw [← tsum_even_add_odd]
      exacts [hₑ, hₒ]
    _ > ∑' n : ℕ, ((2 * n + 1 : ℕ) + 1 : ℝ)⁻¹ + ∑' n : ℕ, ((2 * n + 1 : ℕ) + 1 : ℝ)⁻¹ := by
      gcongr
      refine hₒ.tsum_strict_mono hₑ <| StrongLT.lt fun n ↦ ?_
      simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_one]
      gcongr
      grind
    _ = ∑' n : ℕ, (n + 1 : ℝ)⁻¹ := by
      rw [← two_mul, ← tsum_mul_left]
      congr! 2
      grind
  grind