Quantitative cutoff multiplication for Morrey sources

A bounded multiplier supported in a prescribed set only uses the Morrey norm of the source restricted to that set. Lowering the integrability exponent then supplies the differentiated heat-source norm, including after truncation to nonpositive times.

theorem CKN.Core.Endgame.morrey_norm_mul_le_indicator (P τ C : ℝ) (hP : 0 < P) (hC : 0 ≤ C) (S : Set Foundation.Parabolic.ParabolicPoint) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : ∀ (z : Foundation.Parabolic.ParabolicPoint), |a z| ≤ C) (hsupp : ∀ z ∉ S, a z = 0) : (Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => a z * f z) ≤ ENNReal.ofReal C * Foundation.Parabolic.Morrey.morreyNorm P τ (S.indicator f)

A bounded supported multiplier is controlled by the indicated source norm. No measurability assumption is needed for this upper-integral bound.

theorem CKN.Core.Endgame.cutoff_source_lower_integrability_bound (C : ℝ) (KU : ENNReal) (hC : 0 ≤ C) (S : Set Foundation.Parabolic.ParabolicPoint) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : ∀ (z : Foundation.Parabolic.ParabolicPoint), |a z| ≤ C) (hsupp : ∀ z ∉ S, a z = 0) (hf : AEMeasurable (S.indicator f) MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3) (S.indicator f) ≤ KU) : (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) => a z * f z) ≤ ENNReal.ofReal C * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KU)

A bounded cutoff times an indicated (3,25/3) source has an explicit (6/5,25/3) Morrey bound.

theorem CKN.Core.Endgame.past_derivative_source_morrey_le (C : ℝ) (KU : ENNReal) (hC : 0 ≤ C) (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (j i : Fin 3) (hder : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → |spatialPartial φ j z| ≤ C) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → spatialPartial φ j z = 0) (hu : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => -2 * spatialPartial φ j z * u z i) ≤ ENNReal.ofReal (2 * C) * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KU)

The past-time differentiated source -2 ∂ⱼφ uᵢ has the explicit Morrey bound supplied by a past derivative bound and the initial velocity component norm on the intermediate cylinder.