A006: ∫₀^{π/4} log cos x dx and ∫₀^{π/4} log sin x dx

• LeanPolyLog.Proofs.A006_cos: ∫₀^{π/4} log cos x dx = G/2 - (π/4) log 2.
• LeanPolyLog.Proofs.A006_sin: ∫₀^{π/4} log sin x dx = -G/2 - (π/4) log 2.

Both follow from the sum and the difference of the two integrals, which are computed in LeanPool.PolylogIntegrals.Lemmas.LogTrig:

• ∫₀^{π/4} log sin + ∫₀^{π/4} log cos = -(π/2) log 2;
• ∫₀^{π/4} log cos - ∫₀^{π/4} log sin = G.

theorem LeanPolyLog.Proofs.A006_cos : ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.cos x) = G / 2 - Real.pi / 4 * Real.log 2

A006 (first half): ∫₀^{π/4} log cos x dx = G/2 - (π/4) log 2.

theorem LeanPolyLog.Proofs.A006_sin : ∫ (x : ℝ) in 0..Real.pi / 4, Real.log (Real.sin x) = -G / 2 - Real.pi / 4 * Real.log 2

A006 (second half): ∫₀^{π/4} log sin x dx = -G/2 - (π/4) log 2.