UniformActualCells.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.multiplicativeCell line 17
Source documentation
The multiplicative cell with positive center s, exactly the cell of bounds.tex:219: no choice of transverse normalization occurs in this set.
```
def multiplicativeCell {k : ℕ} (s : Space k) : Set (Space k) :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.multiplicativeCell_eq_image line 20

theorem OAI.AffineBernstein.maximal_model_uniform_actual_cells line 46

Source documentation

Uniform full actual-sigma mass of every multiplicative cell for a maximal model. The constant is independent of the model, its approximating coordinates, and the position of the cell. The eventual threshold may depend on the cell. This is the missing quantitative geometric producer, not a hypothesis about sigma mass. The sole maximality condition is the source's selection of the largest possible number of orthant directions.

theorem maximal_model_uniform_actual_cells {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)
    (hmax : ∀ d' : ℕ, m = d'+1 → ∀ C' : Set (Space (k+1) × Space d'),
      IsModelShape C' → InAffineLimitFamily (sourceEpigraph Ω u) C' → False) :
    ∃ Cσ : ℝ≥0∞, Cσ ≠ ⊤ ∧
      ∀ (C : Set (Space k × Space m)), IsModelShape C →
…

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