OAI/Analysis/AffineBernstein/NormalizedSigma.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.normalized_model_uniform_actual_sigma line 20

   Source documentation

   A normalized maximal model and local convergence produce the full literal geometric hypotheses of the sigma-cell estimate. The uniform constant is fixed before the model, original solution or approximating affine coordinates.

   theorem normalized_model_uniform_actual_sigma {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)
       {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) :
       ∃ Cσ : ℝ≥0∞, Cσ ≠ ⊤ ∧ ∀ {Ω : Set (Space n)}, IsOpen Ω → Ω.Nonempty → Convex ℝ Ω →
         ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
         (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u → EuclideanGraphComplete Ω u →
         ∀ (a : ℕ → Space n × ℝ) (L : ℕ → (Space k × Space m) ≃L[ℝ] (Space n × ℝ))
         (C : Set (Space k × Space m)), IsModelShape C →
         closedBall 0 r ⊆ modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) →
         modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) ⊆ closedBall 0 R →
   …

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