NoZeroTransverse.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.IsModelShape.zero_transverse_mem line 17
lemma OAI.AffineBernstein.IsModelShape.zero_transverse_orthant line 26
theorem OAI.AffineBernstein.complete_affineMaximal_no_orthant_family line 57
Source documentation
A pure orthant cannot lie in the actual full affine local-limit family.
```
theorem complete_affineMaximal_no_orthant_family {n : ℕ} (hn : 0 < n)
    {Ω : 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) :
    ¬ InAffineLimitFamily (sourceEpigraph Ω u) (ambientOrthant n) := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.ambientOrthant
theorem OAI.AffineBernstein.complete_affineMaximal_model_transverse_pos line 75
Source documentation
The transverse dimension of every actual model is positive; this is the nontrivial m=0 part of the manuscript, using the original PDE cap lower mass.
```
theorem complete_affineMaximal_model_transverse_pos {n k m : ℕ} (hn : 0 < n)
    {Ω : 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)
    {C : Set (Space k × Space m)} (hC : IsModelShape C)
    (hf : InAffineLimitFamily (sourceEpigraph Ω u) C) : 1 ≤ m := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph