OAI/Analysis/AffineBernstein/ProjectiveHemisphere.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.projective_cone_lintegral_eq_global line 15
2. theorem OAI.AffineBernstein.projective_hemisphere_lintegral line 57

   Source comment

   Exact projective-coordinate formula for the genuine Euclidean hemisphere measure. This is proved from Haar polar coordinates and ordinary-volume scaling, not an assumed surface-area/Jacobian identity. The tangent space may have dimension zero.

   theorem projective_hemisphere_lintegral
       (f : WithLp 2 (F × ℝ) → ℝ≥0∞) (hf : Measurable f)
       (hscale : ∀ (x : WithLp 2 (F × ℝ)) (t : ℝ), 0 < t → f (t • x) = f x) :
       (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1,
         if 0 < (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 then f e else 0 ∂volume.toSphere) =
       ∫⁻ x : F, ENNReal.ofReal (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ ^
         (Module.finrank ℝ F+1)) * f (WithLp.toLp 2 (x,(1:ℝ))) := by
   …