WholeSphereProjective.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.sphere_two_projective_lintegral line 22

Source comment

Exact two-chart projective integration on the actual sphere.

theorem sphere_two_projective_lintegral (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E)
    (g : E → ℝ≥0∞) (hg : Measurable g) :
    (∫⁻ e : Metric.sphere (0:E) 1, g e ∂volume.toSphere) =
    (∫⁻ x : F, ENNReal.ofReal (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ ^
      (Module.finrank ℝ F+1)) *
      g (f (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ • WithLp.toLp 2 (x,(1:ℝ))))) +
    (∫⁻ x : F, ENNReal.ofReal (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ ^
      (Module.finrank ℝ F+1)) *
      g (-f (‖WithLp.toLp 2 (x,(1:ℝ))‖⁻¹ • WithLp.toLp 2 (x,(1:ℝ))))) := by
…

theorem OAI.AffineBernstein.affineEpigraph_projective_isometry_inverseArea_density line 51

Source comment

A true affine inverse-energy density in any isometric projective chart; the spherical angular basis can be chosen independently of the planar one.

theorem affineEpigraph_projective_isometry_inverseArea_density {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set S} (hD : IsOpen D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {s : S} (hs : s ∈ D) (bS : Module.Basis ι ℝ S)
    (bE bRef : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E)
    (hlast : bE (Sum.inr ()) = f (WithLp.toLp 2 (0,(1:ℝ)))) (v : ι → ℝ) (x : F) :
    let H := fun q : S × E => homogeneousSupport {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.homogeneousSupport