Time moduli from a space-time flux bound #
A uniform local L^(3/2) bound for the scalar flux in a smooth-test pairing
gives the endpoint-compatible power modulus used in lem:compactness of the CKN manuscript.
theorem
ESS.blowup_limit_interval_pairing_modulus_of_spacetime_flux
{C : Set CKN.Foundation.Parabolic.Vec3}
(hC : IsCompact C)
(a b M : ℝ)
(hM : 0 ≤ M)
(F : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(G : ℕ → ℝ → ℝ)
(hF :
∀ (n : ℕ),
MeasureTheory.MemLp (F n) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (F n) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ ENNReal.ofReal M)
(hformula :
∀ (n : ℕ) (s t : ℝ),
s ∈ Set.Icc a b →
t ∈ Set.Icc a b → s ≤ t → G n t - G n s = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in C ×ˢ Set.Ioc s t, F n z)
(n : ℕ)
(s t : ℝ)
:
A spacetime L^(3/2) flux bound controls its time-integrated pairing on
every subrectangle, with the interval length appearing in the modulus.