OAI/Analysis/AffineBernstein/GeneralPositiveCap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affine_image_after_linear line 20
2. theorem OAI.AffineBernstein.positive_linear_cap_area_of_affine_local_limit line 30

   Source comment

   The positive-cap-area lemma for every nonzero height functional, with no orthogonality or vertical-preserving assumption on the affine images.

   theorem positive_linear_cap_area_of_affine_local_limit {n : ℕ} {Ω : Set (Space n)}
       (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       (L : ℕ → (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : ℕ → Space n × ℝ)
       (hclj : ∀ j, IsClosed ((fun p => L j p+v j) '' sourceEpigraph Ω u))
       (hcvj : ∀ j, Convex ℝ ((fun p => L j p+v j) '' sourceEpigraph Ω u))
       (hnej : ∀ j, ((fun p => L j p+v j) '' sourceEpigraph Ω u).Nonempty)
       {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) :
   …

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