MaximalModelExclusion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.transverseEuclideanIsometry line 18
Source documentation
Choose orthonormal transverse coordinates without changing the Euclidean norm used by the spherical fiber estimates.
```
def transverseEuclideanIsometry {m d : ℕ} (hmd : m = d+1) :
    WithLp 2 (Space d × ℝ) ≃ₗᵢ[ℝ] Space m := by
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.affineMaximal_maximal_model_directions_le_one line 27

Source documentation

Normalization of an actual maximal model, followed by the full sigma mass/growth contradiction, excludes every maximal direction number at least two.

theorem affineMaximal_maximal_model_directions_le_one {n k m : ℕ}
    (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : 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)
    {C : Set (Space k × Space m)} (hC : IsModelShape C)
    (hf : InAffineLimitFamily (sourceEpigraph Ω u) C)
    (hmax : ∀ r d : ℕ, ∀ C' : Set (Space r × Space d),
      IsModelShape C' → InAffineLimitFamily (sourceEpigraph Ω u) C' → r ≤ k) : k ≤ 1 := by
…

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

theorem OAI.AffineBernstein.affineMaximal_model_directions_le_one line 70
Source documentation
Every actual affine-limit model has at most one orthant direction in n=3,...,9. This is Proposition one-direction, including the originally missing producers.
```
theorem affineMaximal_model_directions_le_one {n k m : ℕ}
    (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : 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)
    {C : Set (Space k × Space m)} (hC : IsModelShape C)
    (hf : InAffineLimitFamily (sourceEpigraph Ω u) C) : k ≤ 1 := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph

theorem OAI.AffineBernstein.affineMaximal_section_balance line 89

Source documentation

Full uniform section balance, produced from the original hypotheses.

theorem affineMaximal_section_balance {n : ℕ} (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (hc : EuclideanGraphComplete Ω u) :
    ∃ ρ : ℝ, 0 < ρ ∧ ρ ≤ 1 ∧ SectionBalance Ω u ρ := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance