Short-time Hölder estimates

This file records the time-integration estimates used on backward parabolic intervals. The right-hand side uses Mathlib's extended-valued eLpNorm', which agrees with the usual L^p norm when the latter is finite and keeps the statements valid without an extra integrability hypothesis.

def CKN.backwardInterval (t r : ℝ) : Set ℝ

Backward time interval of parabolic length r ^ 2 ending at t.

Equations

• CKN.backwardInterval t r = Set.Ioc (t - r ^ 2) t

theorem CKN.time_holder {t₀ r ρ : ℝ} (hr : 0 < r) (hrr : r ≤ ρ / 2) {g : ℝ → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀))) (hgn : 0 ≤ᵐ[MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀)] g) : (∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ENNReal.ofReal (g s) ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal r ^ (1 / 3) * MeasureTheory.eLpNorm' g 2 (MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀)) ∧ (∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ENNReal.ofReal (g s) ^ (3 / 2)) ^ (2 / 3) ≤ MeasureTheory.eLpNorm' g (3 / 2) (MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀))

Hölder's inequality on a short backward interval, in the two forms used in the pressure estimates.

theorem CKN.time_holder_q {t₀ r ρ q : ℝ} (hr : 0 < r) (hrr : r ≤ ρ / 2) (hq : 3 / 2 ≤ q) {g : ℝ → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀))) (hgn : 0 ≤ᵐ[MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀)] g) : (∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ENNReal.ofReal (g s) ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal r ^ (2 * (2 / 3 - 1 / q)) * MeasureTheory.eLpNorm' g q (MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀))

Hölder's inequality on a short backward interval with an arbitrary exponent q ≥ 3/2.