Bounds for derivatives of smooth spatial tests

Smooth compactly supported vector tests have finite space-time L∞ derivative bounds on every compact cylinder.

theorem ESS.blowup_limit_smooth_test_derivative_bounds {C : Set CKN.Foundation.Parabolic.Vec3} (hC : IsCompact C) (a b : ℝ) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwsupport : tsupport w ⊆ C) : ∃ (Mtest : ENNReal) (Mdiv : ENNReal), Mtest < ⊤ ∧ Mdiv < ⊤ ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) j z.1) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) j z.1) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mtest) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) i z.1) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) i z.1) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mdiv

Uniform L∞ bounds for the spatial derivatives of a smooth compactly supported test on a compact spacetime cylinder.