OAI/Analysis/AffineBernstein/ActualFiberArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.tubeFullRadiusMatrix_basisFun line 18
2. theorem OAI.AffineBernstein.affineEpigraph_sphere_area_bound line 32

   Source comment

   The uniform fiber-area bound is here derived for the literal affine pullback epigraph of the source solution, not for an abstract tube density. The endpoint transverse dimension one is included.

   theorem affineEpigraph_sphere_area_bound {n m : ℕ} (hm : 1 ≤ m)
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (a : Space n × ℝ) (L : (S × Space m) ≃L[ℝ] (Space n × ℝ))
       {D : Set S} (hD : IsOpen D)
       (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       (hzero : ∀ s ∈ D, (0:Space m) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       {s : S} (hs : s ∈ D) {R : ℝ}
       (hR : ∀ y : Space m, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ R) :
       let H := fun q : S × Space m =>
   …

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