OAI/Analysis/AffineBernstein/NoNormalizedMaximalModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_no_normalized_maximal_model line 18

   Source documentation

   The actual analytic contradiction excludes every normalized maximal model with at least two orthant directions. None of its mass bounds is an assumption.

   theorem affineMaximal_no_normalized_maximal_model {n k m d : ℕ}
       (hn : 3 ≤ n) (hn9 : n ≤ 9) (hk : 2 ≤ 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)
       (hmax : ∀ d' : ℕ, m = d'+1 → ∀ C' : Set (Space (k+1) × Space d'),
         IsModelShape C' → InAffineLimitFamily (sourceEpigraph Ω u) C' → False)
       (a : ℕ → Space n × ℝ) (L : ℕ → (Space k × Space m) ≃L[ℝ] (Space n × ℝ))
       {C : Set (Space k × Space m)} (hC : IsModelShape C)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph