ActualLogMeasure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.tubeLogMassWeight line 17
lemma OAI.AffineBernstein.affineEpigraph_logWeight_regular line 23

def OAI.AffineBernstein.affineEpigraphLogMeasure line 65

Source comment

The paper's sigma measure, pushed to logarithmic coordinates. This definition uses the actual affine epigraph support function, not an abstract model metric.

def affineEpigraphLogMeasure {n k : ℕ} (μ : Measure (Space k)) (D : Set (Space k))
    (Ω : Set (Space n)) (u : Space n → ℝ) (a : Space n × ℝ)
    (L : (Space k × E) ≃L[ℝ] (Space n × ℝ)) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E) :
    Measure (Space k) :=
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.affineMaximal_logMeasure_poincare line 75

Source comment

Actual measure form of Proposition log-inequality, with the Euclidean operator norm of the true derivative in logarithmic coordinates.

theorem affineMaximal_logMeasure_poincare {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) :
    (∫ x, φ x^2 ∂affineEpigraphLogMeasure μ D Ω u a L bE) ≤
…

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