Theorems · Theorem · special functions
integral_log_sin_zero_pi_div_two
∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) = -Real.log 2 * Real.pi / 2
The integral of log ∘ sin on 0 … π/2 equals -log 2 * π / 2.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 273 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites44
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- Set.preimageproof · cited by 4,946
- Compl.complproof · cited by 2,925
- Nat.cast_oneproof · cited by 2,501
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.cast_zeroproof · cited by 1,870
- Real.pistatement and proof · cited by 1,774
- Filter.univ_mem'proof · cited by 1,672
- Filter.mp_memproof · cited by 1,537
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- sub_selfproof · cited by 996
Cited by1
Results whose statement or proof uses this declaration.
- integral_log_sin_zero_piproof · cited by 0