OAI/Analysis/AffineBernstein/WholeGraphAreaTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineEpigraph_whole_graph_area_bound line 29

   Source documentation

   Full graph-area transport above a regular fiber base. The loss is a fixed finite chart multiplicity, chosen before every varying epigraph and affine map. No surjectivity or area transport law is assumed.

   theorem affineEpigraph_whole_graph_area_bound {n : ℕ}
       (bS : OrthonormalBasis ι ℝ S) (bF : OrthonormalBasis κ ℝ F)
       (bRef : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E) (e : Fin n ≃ ι ⊕ κ) :
       ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω →
       ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
       (∀ x ∈ Ω, (hessian u x).PosDef) →
       ∀ (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
         {D : Set S}, IsOpen D →
       (∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
       (∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
       ∀ {Q : Set S}, MeasurableSet Q → Q ⊆ D →
   …

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