Log-trigonometric integrals on [0, π/4]

This file collects the lemmas behind A006, the values of ∫₀^{π/4} log cos x dx and ∫₀^{π/4} log sin x dx.

Main results

• LeanPolyLog.LogTrig.integral_pow_mul_neg_log: ∫₀¹ t^m (-log t) dt = 1/(m+1)².
• LeanPolyLog.LogTrig.integral_neg_log_div_one_add_sq: ∫₀¹ -log t / (1+t²) dt = G.
• LeanPolyLog.LogTrig.integral_log_cos_sub_log_sin: ∫₀^{π/4} (log cos x - log sin x) dx = G.
• LeanPolyLog.LogTrig.integral_log_sin_add_integral_log_cos: ∫₀^{π/4} log sin x dx + ∫₀^{π/4} log cos x dx = -(π/2) log 2.
• LeanPolyLog.LogTrig.integral_log_cos_sub_integral_log_sin: ∫₀^{π/4} log cos x dx - ∫₀^{π/4} log sin x dx = G.

Proof sketch

• The sum: cos x = sin (π/2 - x) turns ∫₀^{π/4} log cos into ∫_{π/4}^{π/2} log sin, and Mathlib knows ∫₀^{π/2} log sin = -(π/2) log 2.
• The difference: the substitution x = arctan t turns it into ∫₀¹ -log t / (1+t²) dt. Expanding 1/(1+t²) = ∑ (-1)ⁿ t²ⁿ and integrating term by term gives ∑ (-1)ⁿ/(2n+1)² = G. The interchange of sum and integral is justified by ∫₀¹ t²ⁿ (-log t) dt = 1/(2n+1)², which is summable.

The moments ∫₀¹ t^m (-log t) dt

noncomputable def LeanPolyLog.LogTrig.powMulNegLogPrimitive (m : ℕ) (x : ℝ) : ℝ

An antiderivative of t ^ m * -log t, namely t^(m+1)/(m+1)² - t^(m+1) log t/(m+1). It is continuous on all of ℝ and vanishes at 0.

Equations

• LeanPolyLog.LogTrig.powMulNegLogPrimitive m x = x ^ (m + 1) / (↑m + 1) ^ 2 - x ^ (m + 1) * Real.log x / (↑m + 1)

theorem LeanPolyLog.LogTrig.hasDerivAt_powMulNegLogPrimitive (m : ℕ) {t : ℝ} (ht : t ≠ 0) : HasDerivAt (powMulNegLogPrimitive m) (t ^ m * -Real.log t) t

Away from 0, the derivative of powMulNegLogPrimitive m is t ^ m * -log t.

theorem LeanPolyLog.LogTrig.continuous_pow_succ_mul_log (m : ℕ) : Continuous fun (x : ℝ) => x ^ (m + 1) * Real.log x

x ^ (m + 1) * log x is continuous, including at 0.

theorem LeanPolyLog.LogTrig.continuous_powMulNegLogPrimitive (m : ℕ) : Continuous (powMulNegLogPrimitive m)

The antiderivative powMulNegLogPrimitive m is continuous.

theorem LeanPolyLog.LogTrig.integrableOn_pow_mul_neg_log (m : ℕ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ m * -Real.log t) (Set.Ioc 0 1) MeasureTheory.volume

t ^ m * -log t is integrable on (0, 1]: it is the nonnegative derivative of a continuous function.

theorem LeanPolyLog.LogTrig.integral_pow_mul_neg_log (m : ℕ) : ∫ (t : ℝ) in 0..1, t ^ m * -Real.log t = 1 / (↑m + 1) ^ 2

∫₀¹ t^m (-log t) dt = 1/(m+1)².

The Catalan integral ∫₀¹ -log t / (1 + t²) dt = G

theorem LeanPolyLog.LogTrig.hasSum_neg_one_pow_mul_pow_mul_neg_log {t : ℝ} (ht : t ∈ Set.Ioc 0 1) : HasSum (fun (n : ℕ) => (-1) ^ n * (t ^ (2 * n) * -Real.log t)) (-Real.log t / (1 + t ^ 2))

On (0, 1], -log t / (1 + t²) = ∑ (-1)ⁿ t²ⁿ (-log t). At t = 1 both sides vanish.

theorem LeanPolyLog.LogTrig.summable_one_div_two_mul_add_one_sq : Summable fun (n : ℕ) => 1 / (2 * ↑n + 1) ^ 2

∑ 1/(2n+1)² converges.

theorem LeanPolyLog.LogTrig.integral_neg_log_div_one_add_sq : ∫ (t : ℝ) in 0..1, -Real.log t / (1 + t ^ 2) = G

∫₀¹ -log t / (1 + t²) dt = G, by termwise integration of ∑ (-1)ⁿ t²ⁿ (-log t).

The integrals of log cos and log sin on [0, π/4]

theorem LeanPolyLog.LogTrig.integral_log_cos_sub_log_sin : ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.cos x) - Real.log (Real.sin x) = G

∫₀^{π/4} (log cos x - log sin x) dx = G, via the substitution x = arctan t.

theorem LeanPolyLog.LogTrig.integral_log_cos_eq_integral_log_sin : ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.cos x) = ∫ (x : ℝ) in Real.pi / 4..Real.pi / 2, Real.log (Real.sin x)

∫₀^{π/4} log cos x dx = ∫_{π/4}^{π/2} log sin x dx, since cos x = sin (π/2 - x).

theorem LeanPolyLog.LogTrig.integral_log_sin_add_integral_log_cos : (∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.sin x)) + ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.cos x) = -(Real.pi / 2 * Real.log 2)

∫₀^{π/4} log sin x dx + ∫₀^{π/4} log cos x dx = -(π/2) log 2.

theorem LeanPolyLog.LogTrig.integral_log_cos_sub_integral_log_sin : (∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.cos x)) - ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.sin x) = G

∫₀^{π/4} log cos x dx - ∫₀^{π/4} log sin x dx = G.