OAI/Analysis/AffineBernstein/ActualLogInequality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_logarithmic_inequality line 21

   Source comment

   Proposition log-inequality for the actual affine-epigraph tube. The positive- orthant pullback is extended by zero, and both sides are literal product integrals with the source logarithmic density. No tube-metric completeness is required.

   theorem affineMaximal_logarithmic_inequality {n k : ℕ} (hn : 3 ≤ n) (hn9 : n ≤ 9)
       (hk : 2 ≤ k) (hkn : k ≤ n) {μ : Measure (Space k)} [μ.IsAddHaarMeasure]
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (hm : AffineMaximalOn Ω u)
       (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)
       {φ : Space k → ℝ} (hφ : ContDiff ℝ ∞ φ) (hc : HasCompactSupport φ)
       (hφD : tsupport φ ⊆ logSpace '' D) :
   …

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