LinearLogTrace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.flatInverseTrace_linear line 15
lemma OAI.AffineBernstein.flatInverseTrace_log_linear line 22

theorem OAI.AffineBernstein.affineEpigraph_global_log_coordinate_identity line 46

Source comment

Compact product base IBP on the actual tube, rather than a formal drift identity.

theorem affineEpigraph_global_log_coordinate_identity {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set S} (hD : IsOpen D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0 : E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (ℓ : S →L[ℝ] ℝ) (hℓ : ∀ s ∈ D, 0 < ℓ s)
    {σ : S → ℝ} (hσ : ContDiff ℝ ∞ σ) (hc : HasCompactSupport σ) (hσD : tsupport σ ⊆ D)
    :
    let H := fun q : S × E => homogeneousSupport {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.homogeneousSupport

theorem OAI.AffineBernstein.tube_log_cutoff_absorption line 100

Source comment

The coordinate-log Young estimate, with constants uniform for 3≤n≤9.

theorem tube_log_cutoff_absorption {n v PP DD EE AA Q PA DA RA : ℝ}
    (hn : 3 ≤ n) (hn9 : n ≤ 9) (hP : 0 ≤ PP) (hD : 0 ≤ DD) (hE : 0 ≤ EE)
    (hA : 0 ≤ AA) (hQ : 0 ≤ Q) (hPA : PA^2 ≤ AA*PP) (hDA : DA^2 ≤ AA*DD)
    (hRA : RA^2 ≤ AA*Q) :
    v^2*AA ≤ 4*v^2*(AA+n*PA+((n+2)/2)*DA)-8*v*RA+
      324*v^2*(1+PP+DD+EE)+16*Q := by
…