OAI/Analysis/AffineBernstein/UniformFlatCap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_uniform_flat_cap_lintegral_bound line 23

   Source documentation

   Uniform inverse-energy bound on the actual entire flat support chart. It is produced by stationarity of the original graph, not by an assumed stationarity equation on the tube. The constant precedes, and is independent of, the varying affine normalization L. All cap-containment inputs are geometric and have their literal original-graph meanings.

   theorem affineMaximal_uniform_flat_cap_lintegral_bound {n : ℕ}
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (e : Fin n ≃ ι ⊕ κ) {ε r R : ℝ}
       (hε : 0 < ε) (hr : 0 < r) (hR : 0 ≤ R) (t₀ t₁ c₀ : ℝ) :
       ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω →
       ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
       (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u →
       ∀ (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
         {B : Set S}, IsOpen B →
       (∀ s ∈ B, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
       (∀ s ∈ B, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
       ∀ (q₀ : S × E), inner ℝ q₀.2 (bE (Sum.inr ())) = 1 →
   …

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