OAI/Analysis/AffineBernstein/ProjectiveNormalized.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.projective_hemisphere_normalized_lintegral line 17

   Source comment

   The projective hemisphere formula for an arbitrary measurable integrand, with the normalization map written explicitly.

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

2. theorem OAI.AffineBernstein.projective_hemisphere_density_lintegral line 43

   Source comment

   Substitution of a pointwise density identity into the exact hemisphere formula. The density law need only hold on this chart, and the tangent space may be zero-dimensional.

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