OAI/Analysis/AffineBernstein/CompletePositiveCapFurther.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineSourceEpigraph_convex line 17
2. lemma OAI.AffineBernstein.affineSourceEpigraph_closed line 26
3. theorem OAI.AffineBernstein.complete_affineMaximal_positive_cap_area line 37

   Source comment

   Source positive-cap-area lemma (bounds.tex:18–126) for the actual affine images of the original complete graph, with all image hypotheses derived.

   theorem complete_affineMaximal_positive_cap_area {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) :
       ∃ c > 0, ∀ᶠ j in atTop, c ≤ affineImageLinearCapArea Ω u (L j) (v j) ell b := by
   …

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