Series helpers

Elementary series identities and bounds shared by the proofs of A001, A004 and A005.

Main results

• LeanPolyLog.Series.hasSum_one_div_odd_sq: ∑_{k ≥ 0} 1/(2k+1)² = π²/8.
• LeanPolyLog.Series.hasSum_eta_two: η(2) = ∑_{n ≥ 0} (-1)ⁿ/(n+1)² = π²/12.
• LeanPolyLog.Series.hasSum_catalan: the series defining G converges (absolutely) to G.
• LeanPolyLog.Series.hasSum_log_one_add_sq_div: for 0 < x < 1, log(1+x²)/x = ∑_{n ≥ 0} (-1)ⁿ x^(2n+1)/(n+1).
• LeanPolyLog.Series.continuous_log_one_add_sq_div and LeanPolyLog.Series.continuous_log_one_add_sq_sq_div_cube: log(1+x²)/x and log²(1+x²)/x³ are continuous on all of ℝ. At x = 0 Lean's division gives the value 0, which is also the limit, because 0 ≤ log(1+x²) ≤ x².

Values of ζ(2)-type series

theorem LeanPolyLog.Series.hasSum_one_div_even_sq : HasSum (fun (k : ℕ) => 1 / ↑(2 * k) ^ 2) (Real.pi ^ 2 / 24)

The even terms of ζ(2), indexed as n = 2k (the k = 0 term is 1/0 = 0).

theorem LeanPolyLog.Series.summable_one_div_odd_sq : Summable fun (k : ℕ) => 1 / ↑(2 * k + 1) ^ 2

The odd terms of ζ(2), indexed as n = 2k + 1, are summable.

theorem LeanPolyLog.Series.hasSum_one_div_odd_sq_natCast : HasSum (fun (k : ℕ) => 1 / ↑(2 * k + 1) ^ 2) (Real.pi ^ 2 / 8)

∑_{k ≥ 0} 1/(2k+1)² = π²/8, with the index cast from ℕ as in f (2 * k + 1).

theorem LeanPolyLog.Series.hasSum_one_div_odd_sq : HasSum (fun (k : ℕ) => 1 / (2 * ↑k + 1) ^ 2) (Real.pi ^ 2 / 8)

∑_{k ≥ 0} 1/(2k+1)² = π²/8.

theorem LeanPolyLog.Series.hasSum_eta_two : HasSum (fun (n : ℕ) => (-1) ^ n / (↑n + 1) ^ 2) (Real.pi ^ 2 / 12)

The Dirichlet eta function at 2: η(2) = ∑_{n ≥ 0} (-1)ⁿ/(n+1)² = π²/12.

theorem LeanPolyLog.Series.hasSum_catalan : HasSum (fun (k : ℕ) => (-1) ^ k / (2 * ↑k + 1) ^ 2) G

The series defining Catalan's constant converges (absolutely), with sum G.

The function log(1 + x²)

theorem LeanPolyLog.Series.log_one_add_sq_nonneg (x : ℝ) : 0 ≤ Real.log (1 + x ^ 2)

log(1+x²) ≥ 0.

theorem LeanPolyLog.Series.log_one_add_sq_le_sq (x : ℝ) : Real.log (1 + x ^ 2) ≤ x ^ 2

log(1+x²) ≤ x², from log y ≤ y - 1.

theorem LeanPolyLog.Series.hasSum_log_one_add_sq_div {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : HasSum (fun (n : ℕ) => (-1) ^ n / (↑n + 1) * x ^ (2 * n + 1)) (Real.log (1 + x ^ 2) / x)

The power series of log(1+x²)/x on (0, 1): ∑_{n ≥ 0} (-1)ⁿ x^(2n+1)/(n+1).

theorem LeanPolyLog.Series.continuous_of_norm_le_of_tendsto_zero {f g : ℝ → ℝ} (hf : ∀ (x : ℝ), x ≠ 0 → ContinuousAt f x) (hf0 : f 0 = 0) (hle : ∀ (x : ℝ), ‖f x‖ ≤ g x) (hg : Filter.Tendsto g (nhds 0) (nhds 0)) : Continuous f

A function f : ℝ → ℝ that is continuous away from 0, vanishes at 0 and is dominated by a function tending to 0 at 0 is continuous.

theorem LeanPolyLog.Series.continuous_log_one_add_sq_div : Continuous fun (x : ℝ) => Real.log (1 + x ^ 2) / x

x ↦ log(1+x²)/x is continuous on ℝ (its value at 0 is 0).

theorem LeanPolyLog.Series.continuous_log_one_add_sq_sq_div_cube : Continuous fun (x : ℝ) => Real.log (1 + x ^ 2) ^ 2 / x ^ 3

x ↦ log²(1+x²)/x³ is continuous on ℝ (its value at 0 is 0).