OAI/Analysis/AffineBernstein/PositiveFaceLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.LocalDistanceConverges.eventually_support_coordinate_lower line 23
2. theorem OAI.AffineBernstein.complete_affineMaximal_positive_face_mass line 49

   Source comment

   The exact positive boundary mass left after removing all finitely many face strips, uniformly along affine local limits. This is before tube charts; the integral remains the literal original-graph affine area.

   theorem complete_affineMaximal_positive_face_mass {n k : ℕ} (hn : 0 < n)
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       (hc : EuclideanGraphComplete Ω u)
       (L : ℕ → (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : ℕ → Space n × ℝ)
       {C : Set (Space n × ℝ)} (hC : IsClosed C)
       (hlim : LocalDistanceConverges (fun j => (fun p => L j p+v j) '' sourceEpigraph Ω u) C)
       (ell : (Space n × ℝ) →L[ℝ] ℝ) (hell : ell ≠ 0)
       {b : ℝ} (hcapC : Bornology.IsBounded (C ∩ {z | ell z ≤ b}))
       {o : Space n × ℝ} (ho : o ∈ interior C) (hob : ell o < b)
       (s : Fin k → Fin n ⊕ Unit) (hs : ∀ z ∈ C, ∀ i, 0 ≤ ambientCoordinates n z (s i)) :
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.ambientCoordinates