Archimedes' angular marginal

The height coordinate of uniform sphere probability is uniform on [-1,1].

Archimedes' hat-box identity for every Euclidean unit direction.

theorem LiebThirring.sphereHeight_uniform : MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => (↑ω).ofLp 2) unitSphereMeasure = (ENNReal.ofReal 2)⁻¹ • MeasureTheory.volume.restrict (Set.Icc (-1) 1)

The height coordinate of uniform sphere probability is uniform on [-1,1].

theorem LiebThirring.unitSphereMeasure_inner_uniform (e : Position) (he : ‖e‖ = 1) : MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => inner ℝ (↑ω) e) unitSphereMeasure = (ENNReal.ofReal 2)⁻¹ • MeasureTheory.volume.restrict (Set.Icc (-1) 1)

Archimedes' hat-box identity for every Euclidean unit direction.