PositiveLimitCap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.positive_cap_area_of_affine_local_limit line 20

Source comment

Positive cap area for a local limit of genuine affine images. This is bounds.tex, Lemma positive-cap-area, with a strict height cutoff (hence it also bounds the closed cap whenever that area is expressed as a measure).

theorem positive_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)
    {b : ℝ} (hcapC : Bornology.IsBounded (C ∩ {z | z.2 ≤ b}))
    {o : Space n × ℝ} (ho : o ∈ interior C) (hob : o.2 < b) :
    ∃ c > 0, ∀ᶠ j in atTop, c ≤ affineImageCapArea Ω u (L j) (v j) b := by
…

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