OAI/Analysis/AffineBernstein/ModelPositiveSigma.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.positiveClosedRectangle line 19
2. lemma OAI.AffineBernstein.isCompact_positiveClosedRectangle line 22
3. theorem OAI.AffineBernstein.normalized_model_positive_sigma_rectangle line 33

   Source documentation

   The face mass cannot disappear in the true weighted sigma measure. This is an eventual lower bound on one fixed physical rectangle, derived from the original PDE and Euclidean graph completeness, not a mass premise.

   theorem normalized_model_positive_sigma_rectangle {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