The integral ∫₀^{π/4} x log (2 + 2 cos 2x) dx

This file computes ∫₀^{π/4} x log (2 + 2 cos 2x) dx = (π/4) G - (21/64) ζ(3), the heart of A007 (and hence of A008 and A009), by an Abel-limit argument.

Main results

• LeanPolyLog.Fourier.hasSum_neg_pow_mul_cos_div: for 0 ≤ r < 1, ∑_{n ≥ 1} (-r)ⁿ cos (nθ) / n = -log (1 + 2r cos θ + r²) / 2.
• LeanPolyLog.Fourier.integral_mul_cos_two_mul: ∫₀^{π/4} x cos (2nx) dx = (π/8) sin (nπ/2) / n + (cos (nπ/2) - 1) / (4n²) for n ≠ 0.
• LeanPolyLog.Fourier.hasSum_integral_mul_log: for 0 ≤ r < 1, ∫₀^{π/4} x log (1 + 2r cos 2x + r²) dx = ∑ₙ coeff n * rⁿ.
• LeanPolyLog.Fourier.hasSum_one_div_odd_cube: ∑_{k ≥ 0} 1/(2k+1)³ = (7/8) ζ(3).
• LeanPolyLog.Fourier.hasSum_coeff: ∑ₙ coeff n = (π/4) G - (21/64) ζ(3).
• LeanPolyLog.Fourier.integral_mul_log_two_add_two_cos: ∫₀^{π/4} x log (2 + 2 cos 2x) dx = (π/4) G - (21/64) ζ(3).

Proof sketch

• For 0 ≤ r < 1, the real part of ∑ zⁿ/n = -log (1 - z) at z = -r e^{iθ} is the cosine series of log (1 + 2r cos θ + r²) above. Its terms are bounded by rⁿ, so after putting θ = 2x and multiplying by x it can be integrated term by term over [0, π/4]. This writes L(r) = ∫₀^{π/4} x log (1 + 2r cos 2x + r²) dx as a power series ∑ coeff n * rⁿ.
• The complex logarithm is never used at r = 1. Instead, L is continuous at r = 1 by dominated convergence (for x ∈ [0, π/4] and r near 1 the argument of the logarithm lies in [1, 9]), and the power series tends to ∑ coeff n as r → 1⁻ by Abel's limit theorem (Real.tendsto_tsum_powerSeries_nhdsWithin_lt). Hence L(1) = ∑ coeff n.
• Splitting n by its residue mod 4, the sin (nπ/2) terms give (π/4) G and the cos (nπ/2) terms give -(1/2 - 1/8) ∑ 1/(2k+1)³ = -(21/64) ζ(3).

theorem LeanPolyLog.Fourier.sq_norm_one_add_mul_exp (r θ : ℝ) : ‖1 + ↑r * Complex.exp (↑θ * Complex.I)‖ ^ 2 = 1 + 2 * r * Real.cos θ + r ^ 2

‖1 + r e^{iθ}‖² = 1 + 2 r cos θ + r².

theorem LeanPolyLog.Fourier.re_neg_mul_exp_pow (r θ : ℝ) (n : ℕ) : ((-↑r * Complex.exp (↑θ * Complex.I)) ^ n).re = (-r) ^ n * Real.cos (↑n * θ)

The real part of (-r e^{iθ})ⁿ is (-r)ⁿ cos (nθ).

theorem LeanPolyLog.Fourier.hasSum_neg_pow_mul_cos_div {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (θ : ℝ) : HasSum (fun (n : ℕ) => (-r) ^ n * Real.cos (↑n * θ) / ↑n) (-(Real.log (1 + 2 * r * Real.cos θ + r ^ 2) / 2))

For 0 ≤ r < 1: ∑_{n ≥ 1} (-r)ⁿ cos (nθ) / n = -log (1 + 2 r cos θ + r²) / 2. The n = 0 term is 0 because Lean divides by 0. This is the real part of ∑ zⁿ/n = -log (1 - z) at z = -r e^{iθ}.

The integrals ∫₀^{π/4} x cos (2nx) dx

theorem LeanPolyLog.Fourier.integral_mul_cos_two_mul {n : ℕ} (hn : n ≠ 0) : ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.cos (2 * ↑n * x) = Real.pi / 8 * Real.sin (↑n * Real.pi / 2) / ↑n + (Real.cos (↑n * Real.pi / 2) - 1) / (4 * ↑n ^ 2)

∫₀^{π/4} x cos (2nx) dx = (π/8) sin (nπ/2) / n + (cos (nπ/2) - 1) / (4n²) for n ≠ 0.

Termwise integration for r < 1

noncomputable def LeanPolyLog.Fourier.coeff (n : ℕ) : ℝ

The coefficients of ∫₀^{π/4} x log (1 + 2r cos 2x + r²) dx as a power series in r.

Equations

• LeanPolyLog.Fourier.coeff n = -2 * (-1) ^ n / ↑n * ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.cos (2 * ↑n * x)

theorem LeanPolyLog.Fourier.hasSum_mul_log {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (x : ℝ) : HasSum (fun (n : ℕ) => -2 * (-r) ^ n / ↑n * (x * Real.cos (2 * ↑n * x))) (x * Real.log (1 + 2 * r * Real.cos (2 * x) + r ^ 2))

For 0 ≤ r < 1: x log (1 + 2r cos 2x + r²) = ∑ₙ (-2 (-r)ⁿ / n) x cos (2nx).

theorem LeanPolyLog.Fourier.norm_term_le {r : ℝ} (hr0 : 0 ≤ r) (n : ℕ) {x : ℝ} (hx : x ∈ Set.Ioc 0 (Real.pi / 4)) : ‖-2 * (-r) ^ n / ↑n * (x * Real.cos (2 * ↑n * x))‖ ≤ 2 * r ^ n * (Real.pi / 4)

The terms of the series in hasSum_mul_log are bounded by 2 rⁿ (π/4) on (0, π/4].

theorem LeanPolyLog.Fourier.hasSum_integral_mul_log {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : HasSum (fun (n : ℕ) => coeff n * r ^ n) (∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (1 + 2 * r * Real.cos (2 * x) + r ^ 2))

For 0 ≤ r < 1: ∫₀^{π/4} x log (1 + 2r cos 2x + r²) dx = ∑ₙ coeff n * rⁿ.

Continuity at r = 1 and Abel's limit

theorem LeanPolyLog.Fourier.one_le_and_le_nine {r x : ℝ} (hr : r ∈ Set.Ioo 0 2) (hx : x ∈ Set.Ioc 0 (Real.pi / 4)) : 1 ≤ 1 + 2 * r * Real.cos (2 * x) + r ^ 2 ∧ 1 + 2 * r * Real.cos (2 * x) + r ^ 2 ≤ 9

For 0 < r < 2 and x ∈ (0, π/4]: 1 ≤ 1 + 2r cos 2x + r² ≤ 9.

theorem LeanPolyLog.Fourier.continuousAt_integral_mul_log : ContinuousAt (fun (r : ℝ) => ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (1 + 2 * r * Real.cos (2 * x) + r ^ 2)) 1

r ↦ ∫₀^{π/4} x log (1 + 2r cos 2x + r²) dx is continuous at r = 1, by dominated convergence: for r near 1 the integrand is bounded by (π/4) log 9.

theorem LeanPolyLog.Fourier.integral_mul_log_eq_of_hasSum {S : ℝ} (hS : HasSum coeff S) : ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (1 + 2 * 1 * Real.cos (2 * x) + 1 ^ 2) = S

Abel's limit: if ∑ coeff n = S, then ∫₀^{π/4} x log (2 + 2 cos 2x) dx = S.

The sum of the coefficients

theorem LeanPolyLog.Fourier.hasSum_zeta3 : HasSum (fun (n : ℕ) => 1 / (↑n + 1) ^ 3) zeta3

The series defining ζ(3) converges to zeta3.

theorem LeanPolyLog.Fourier.hasSum_one_div_natCast_cube : HasSum (fun (n : ℕ) => 1 / ↑n ^ 3) zeta3

∑_{n ≥ 0} 1/n³ = ζ(3), where the n = 0 term is 1/0 = 0.

theorem LeanPolyLog.Fourier.hasSum_one_div_odd_cube : HasSum (fun (k : ℕ) => 1 / (2 * ↑k + 1) ^ 3) (7 / 8 * zeta3)

∑_{k ≥ 0} 1/(2k+1)³ = (7/8) ζ(3).

theorem LeanPolyLog.Fourier.coeff_odd (k : ℕ) : coeff (2 * k + 1) = Real.pi / 4 * ((-1) ^ k / (2 * ↑k + 1) ^ 2) - 1 / 2 * (1 / (2 * ↑k + 1) ^ 3)

The odd coefficients: coeff (2k+1) = (π/4) (-1)ᵏ/(2k+1)² - 1/(2 (2k+1)³).

theorem LeanPolyLog.Fourier.coeff_even (k : ℕ) : coeff (2 * k) = (1 - (-1) ^ k) / (16 * ↑k ^ 3)

The even coefficients: coeff (2k) = (1 - (-1)ᵏ) / (16 k³).

theorem LeanPolyLog.Fourier.hasSum_coeff : HasSum coeff (Real.pi / 4 * G - 21 / 64 * zeta3)

∑ₙ coeff n = (π/4) G - (21/64) ζ(3).

theorem LeanPolyLog.Fourier.integral_mul_log_two_add_two_cos : ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (1 + 2 * 1 * Real.cos (2 * x) + 1 ^ 2) = Real.pi / 4 * G - 21 / 64 * zeta3

∫₀^{π/4} x log (2 + 2 cos 2x) dx = (π/4) G - (21/64) ζ(3).