OAI/Analysis/AffineBernstein/AffineCapArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.exists_uniform_positive_affine_cap_area line 19

   Source comment

   Uniform positive area for genuine affine images of the original solution. The only uniform geometric data are a bounded compact cap and an interior ball strictly below its top. This joins the source ray, shear and smooth-cap arguments.

   theorem exists_uniform_positive_affine_cap_area (n : ℕ) {ε r R : ℝ}
       (hε : 0 < ε) (hr : 0 < r) (hR : 0 ≤ R) :
       ∃ C : ℝ, 0 < C ∧ ∀ (Ω : Set (Space n)) (u : Space n → ℝ)
         (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v o : Space n × ℝ) (b : ℝ),
         IsOpen Ω → ContDiffOn ℝ ∞ u Ω →
         (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u →
         IsCompact {z | z ∈ (fun p => L p+v) '' sourceEpigraph Ω u ∧ z.2 ≤ b} →
         (∀ z ∈ (fun p => L p+v) '' sourceEpigraph Ω u, z.2 ≤ b → ‖z‖ ≤ R) →
         (Metric.ball o r ⊆ (fun p => L p+v) '' sourceEpigraph Ω u) →
         o.2 ≤ b-6*ε → C ≤ affineImageCapArea Ω u L v b := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.affineImageCapArea