OAI/Analysis/AffineBernstein/LinearSphere.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.linear_cone_lintegral line 18
2. lemma OAI.AffineBernstein.sphere_lintegral_linear_jacobian line 98

   Source comment

   Exact projective change of variables on Haar-normalized sphere area. The Jacobian is derived from the linear volume determinant and polar coordinates. The ambient integrand is homogeneous of degree zero; no integrability is assumed.

   lemma sphere_lintegral_linear_jacobian (μ : Measure E) [μ.IsAddHaarMeasure]
       [Nontrivial E] (A : E ≃L[ℝ] E) (f : E → ℝ≥0∞) (hf : Measurable f)
       (hscale : ∀ (x : E) (r : ℝ), 0 < r → f (r • x) = 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‖⁻¹)^(Module.finrank ℝ E)) ∂μ.toSphere := by
   …