ActualLogGrowth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.tsupport_logarithmicCutoff_subset line 23

lemma OAI.AffineBernstein.affineEpigraphLogMeasure_box_finite line 32

Source comment

Finiteness on each available logarithmic box follows from the literal support-function density, without any a priori integral bound.

lemma affineEpigraphLogMeasure_box_finite {n k : ℕ}
    {μ : Measure (Space k)} [μ.IsAddHaarMeasure]
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (Space k × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set (Space k)} (hD : IsOpen D) (hDpos : D ⊆ positiveOrthant k)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0 : E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E) {R : ℝ}
    (hR : logarithmicBox k R ⊆ logSpace '' D) :
    affineEpigraphLogMeasure μ D Ω u a L bE (logarithmicBox k R) ≠ ⊤ := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.positiveOrthant, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.logarithmicBox, OAI.AffineBernstein.logSpace, OAI.AffineBernstein.affineEpigraphLogMeasure

theorem OAI.AffineBernstein.affineMaximal_no_polynomial_logMeasure line 51

Source comment

The growth contradiction is now specialized to genuine affine-maximal approximate graphs. Only the two remaining quantitative model bounds are inputs: positive mass on one fixed box and a uniform polynomial upper bound. Every Poincare estimate and local finiteness assertion is derived here.

theorem affineMaximal_no_polynomial_logMeasure {n k l₀ : ℕ}
    (hn : 3 ≤ n) (hn9 : n ≤ 9) (hk : 2 ≤ k) (hkn : k ≤ n)
    {μ : Measure (Space k)} [μ.IsAddHaarMeasure]
    (Ω : ℕ → Set (Space n)) (u : ℕ → Space n → ℝ)
    (a : ℕ → Space n × ℝ) (L : ℕ → (Space k × E) ≃L[ℝ] (Space n × ℝ))
    (D : ℕ → Set (Space k)) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (hΩ : ∀ j, IsOpen (Ω j)) (hcv : ∀ j, Convex ℝ (Ω j))
    (hu : ∀ j, ContDiffOn ℝ ∞ (u j) (Ω j))
    (hp : ∀ j x, x ∈ Ω j → (hessian (u j) x).PosDef)
    (hm : ∀ j, AffineMaximalOn (Ω j) (u j))
    (hD : ∀ j, IsOpen (D j)) (hDpos : ∀ j, D j ⊆ positiveOrthant k)
    (hK : ∀ j s, s ∈ D j → IsCompact {y | (s,y) ∈ affineEpigraphPullback (Ω j) (u j) (a j) (L j)})
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.positiveOrthant, OAI.AffineBernstein.affineEpigraphPullback