OAI/Analysis/AffineBernstein/HomogeneousSphere.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.sphere_lintegral_homogeneous_linear line 20

   Source comment

   The projective sphere Jacobian cancels a homogeneous density of degree `-(dim E - 1)`, leaving precisely one inverse norm.

   lemma sphere_lintegral_homogeneous_linear (μ : Measure E) [μ.IsAddHaarMeasure]
       (A : E ≃L[ℝ] E) (f : E → ℝ≥0∞) (hf : Measurable f)
       (hscale : ∀ (x : E), x ≠ 0 → ∀ (r : ℝ), 0 < r →
         f (r • x) = ENNReal.ofReal ((r⁻¹)^(Module.finrank ℝ E - 1)) * f x) :
       (∫⁻ e : Metric.sphere (0:E) 1, f e ∂μ.toSphere) =
         ENNReal.ofReal |A.toLinearMap.det| *
           ∫⁻ e : Metric.sphere (0:E) 1,
             f (A e) * ENNReal.ofReal (‖A e‖⁻¹) ∂μ.toSphere := by
   …