OAI/Analysis/AffineBernstein/ProjectiveCone.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.projective_cone_lintegral line 19

   Source comment

   Ordinary-volume computation of a projective cone. Together with polar coordinates this yields the hemisphere chart density without assuming a surface-area formula.

   theorem projective_cone_lintegral (f : WithLp 2 (F × ℝ) → ℝ≥0∞) (hf : Measurable f)
       (hscale : ∀ (x : WithLp 2 (F × ℝ)) (t : ℝ), 0 < t → f (t • x) = f x) :
       (∫⁻ t in Ioi (0:ℝ), ∫⁻ x : F,
         if ‖WithLp.toLp 2 (x,t)‖ < 1 then f (WithLp.toLp 2 (x,t)) else 0) =
           ∫⁻ x : F, ENNReal.ofReal (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ ^
             (Module.finrank ℝ F+1) / (Module.finrank ℝ F+1)) * f (WithLp.toLp 2 (x,(1:ℝ))) := by
   …

2. lemma OAI.AffineBernstein.sphere_lintegral_mul_radial_eq line 81

   Source comment

   A homogeneous quantity which expands on inward rays has its spherical integral controlled by its integral over the punctured unit ball. The exact radial Haar normalization is retained.

   lemma sphere_lintegral_mul_radial_eq {E : Type*} [NormedAddCommGroup E]
       [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
       (μ : Measure E) [μ.IsAddHaarMeasure] {f : E → ℝ≥0∞}
       (hf : Measurable (fun e : Metric.sphere (0:E) 1 => f e))
       (hscale : ∀ (e : Metric.sphere (0:E) 1) (r : ℝ), 0 < r → r < 1 → f e = f (r • (e:E))) :
       (∫⁻ e : Metric.sphere (0:E) 1, f e ∂μ.toSphere) *
         ENNReal.ofReal (1 / ((Module.finrank ℝ E - 1 + 1 : ℕ):ℝ)) =
           ∫⁻ x in Metric.ball (0:E) 1 \ {0}, f x ∂μ := by
   …