OAI/Analysis/AffineBernstein/CapArea.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.integrableOn_affineArea_sublevel line 14
2. theorem OAI.AffineBernstein.affineMaximal_cap_area_comparison line 27

   Source documentation

   Local weak maximization and a smooth convex replacement give the cap comparison on its actual open base.

   theorem affineMaximal_cap_area_comparison {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
       {u q : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (hq : ContDiffOn ℝ ∞ q Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hmax : AffineMaximalOn Ω u)
       {b ε : ℝ} (hε : 0 < ε) (hK : IsCompact {x | x ∈ Ω ∧ u x ≤ b})
       (hqtop : ∀ x, x ∈ Ω → u x < b → q x ≤ b-2*ε)
       (hqp : ∀ x, x ∈ Ω → u x < b → (hessian q x).PosDef)
       {B : Set (Space n)} (hB : IsOpen B)
       (hBE : ∀ x ∈ B, x ∈ Ω ∧ u x < b ∧ ε ≤ q x-u x) :
       (∫ x in B, affineAreaDensity q x) ≤
         ∫ x in {x | x ∈ Ω ∧ u x < b}, affineAreaDensity u x := by
   …

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

3. theorem OAI.AffineBernstein.affineMaximal_positive_cap_area line 76

   Source documentation

   The graph-coordinate positive cap estimate, with a quantitative uniform constant. The original PDE, not an area lower bound, is the hypothesis.

   theorem affineMaximal_positive_cap_area {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hmax : AffineMaximalOn Ω u)
       {b ε α r : ℝ} (hε : 0 < ε) (hα : 0 < α) (_hr : 0 < r)
       (c : Space n) (hK : IsCompact {x | x ∈ Ω ∧ u x ≤ b})
       (hball : ∀ x ∈ Metric.ball c r, x ∈ Ω ∧ u x ≤ b-6*ε)
       (hradius : ∀ x, x ∈ Ω → u x < b → α*‖x-c‖^2 ≤ 2*ε) :
       volume.real (Metric.ball (0 : Space n) r) * Real.rpow (2*α) ((n : ℝ)/((n : ℝ)+2)) ≤
         ∫ x in {x | x ∈ Ω ∧ u x < b}, affineAreaDensity u x := by
   …

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

4. lemma OAI.AffineBernstein.cap_area_constant_pos line 101
5. theorem OAI.AffineBernstein.exists_uniform_positive_graph_cap_area line 111

   Source documentation

   Uniform nonvanishing in uniformly bounded graph caps, without assumptions on boundary regularity or uniform Hessian bounds.

   theorem exists_uniform_positive_graph_cap_area (n : ℕ) {ε r R : ℝ}
       (hε : 0 < ε) (hr : 0 < r) :
       ∃ C : ℝ, 0 < C ∧ ∀ (Ω : Set (Space n)) (u : Space n → ℝ)
         (b : ℝ) (c : Space n), IsOpen Ω → ContDiffOn ℝ ∞ u Ω →
         (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u →
         IsCompact {x | x ∈ Ω ∧ u x ≤ b} →
         (∀ x ∈ Metric.ball c r, x ∈ Ω ∧ u x ≤ b-6*ε) →
         (∀ x, x ∈ Ω → u x < b → ‖x-c‖ ≤ R) →
         C ≤ ∫ x in {x | x ∈ Ω ∧ u x < b}, affineAreaDensity u x := by
   …

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