OAI/Analysis/AffineBernstein/CompleteSphericalCaps.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.complete_affineMaximal_uniform_spherical_cap_bound line 30

   Source documentation

   Full-sphere inverse-energy bound from the unchanged complete original PDE and literal normalized ambient cap geometry. Compactness of the original graph cap and of every fiber is produced here, not assumed. All constants precede the varying affine map and solution.

   theorem complete_affineMaximal_uniform_spherical_cap_bound {n : ℕ}
       (bS : OrthonormalBasis ι ℝ S) (bF : OrthonormalBasis κ ℝ F)
       (bRef : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E) (e : Fin n ≃ ι ⊕ κ)
       (ℓ : S →L[ℝ] ℝ) (o : S × E) {ε r R : ℝ} (hε : 0 < ε) (hr : 0 < r)
       (hR : 0 ≤ R) (t₁ : ℝ) (hogap : ℓ o.1 < t₁+ε) :
       ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Ω.Nonempty → Convex ℝ Ω →
         ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
         (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u → EuclideanGraphComplete Ω u →
         ∀ (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
           {B : Set S}, IsOpen B → (∀ s ∈ B, ℓ s ≤ t₁+ε) →
         (∀ s ∈ B, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
   …

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