OAI/Analysis/AffineBernstein/ActualHemisphereInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineEpigraph_hemisphere_inverseArea_lintegral line 26

   Source comment

   Exact hemisphere/flat-chart transport of the actual affine inverse metric area, with the true Haar sphere measure and the true support conormal. No surface-Jacobian, curvature, or inverse-metric law is assumed.

   theorem affineEpigraph_hemisphere_inverseArea_lintegral {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 × WithLp 2 (F × ℝ)) ≃L[ℝ] (Space n × ℝ))
       {D : Set S} (hD : IsOpen D)
       (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       (hzero : ∀ s ∈ D, (0 : WithLp 2 (F × ℝ)) ∈
         interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       {s : S} (hs : s ∈ D)
       (bS : Module.Basis ι ℝ S)
       (bE : OrthonormalBasis (κ ⊕ Unit) ℝ (WithLp 2 (F × ℝ)))
       (hlast : bE (Sum.inr ()) = WithLp.toLp 2 (0,(1:ℝ))) (v : ι → ℝ) :
   …

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