OAI/Analysis/AffineBernstein/ModelPositiveLogMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.positiveClosedRectangle_sub_logBox line 17
2. theorem OAI.AffineBernstein.normalized_model_positive_log_mass line 34

   Source documentation

   A fixed log box has strictly positive actual sigma mass, uniformly along any normalized actual epigraph approximation. Local finiteness is proved from smooth compact fibers, and the positive mass is produced from the original PDE.

   theorem normalized_model_positive_log_mass {n k m d : ℕ} (hn : 1 ≤ n) (hk : 1 ≤ k)
       (hm : 1 ≤ m) (e : Fin n ≃ Fin k ⊕ Fin d) (eE : Fin m ≃ Fin d ⊕ Unit)
       (f : WithLp 2 (Space d × ℝ) ≃ₗᵢ[ℝ] Space m)
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hmP : AffineMaximalOn Ω u)
       (hcomplete : EuclideanGraphComplete Ω u)
       (a : ℕ → Space n × ℝ) (L : ℕ → (Space k × Space m) ≃L[ℝ] (Space n × ℝ))
       {C : Set (Space k × Space m)} (hC : IsModelShape C)
       (hlim : LocalDistanceConverges (fun j => affineEpigraphPullback Ω u (a j) (L j)) C)
       {r R₀ : ℝ} (hr : 0 < r)
       (hin : closedBall (0:Space m) r ⊆ modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.modelFiber