Causal bounded multipliers for linear heat sources

Indicated input measurability suffices for a supported product after truncation to the past. Uniform multiplier bounds control its Morrey norm. The improved velocity exponent supplies the linear velocity terms, while a cutoff of absolute value at most one preserves pressure-gradient bounds.

noncomputable def CKN.Core.Endgame.pastMultiplierSource (a f : Foundation.Parabolic.ParabolicPoint → ℝ) : Foundation.Parabolic.ParabolicPoint → ℝ

A scalar product restricted to nonpositive times.

Equations

• CKN.Core.Endgame.pastMultiplierSource a f = {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => a z * f z

theorem CKN.Core.Endgame.pastMultiplierSource_zero_outside_intermediate {a f : Foundation.Parabolic.ParabolicPoint → ℝ} (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → a z = 0) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) : pastMultiplierSource a f z = 0

The support of the past product lies in the intermediate cylinder.

theorem CKN.Core.Endgame.pastMultiplierSource_aemeasurable {a f : Foundation.Parabolic.ParabolicPoint → ℝ} (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f) MeasureTheory.volume) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → a z = 0) : AEMeasurable (pastMultiplierSource a f) MeasureTheory.volume

The causal product is measurable without a global measurability assumption on the original input.

theorem CKN.Core.Endgame.pastMultiplierSource_morrey_le (P τ C : ℝ) (hP : 0 < P) (hC : 0 ≤ C) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (hbound : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → |a z| ≤ C) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → a z = 0) : Foundation.Parabolic.Morrey.morreyNorm P τ (pastMultiplierSource a f) ≤ ENNReal.ofReal C * Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f)

A bounded past multiplier preserves a Morrey exponent pair with its explicit multiplier factor.

theorem CKN.Core.Endgame.causal_linear_velocity_source_morrey_le (q C : ℝ) (KU : ENNReal) (hq : 5 / 2 < q) (hC : 0 ≤ C) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f) MeasureTheory.volume) (hbound : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → |a z| ≤ C) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → a z = 0) (hN : Foundation.Parabolic.Morrey.morreyNorm 3 25 ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f) ≤ KU) : AEMeasurable (pastMultiplierSource a f) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) (pastMultiplierSource a f) ≤ ENNReal.ofReal C * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KU)

An improved (3,25) velocity input supplies each bounded linear source at the paper heat-source exponents, with an explicit coefficient.

theorem CKN.Core.Endgame.causal_linear_pressure_source_morrey_le (q : ℝ) (KP : ENNReal) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f) MeasureTheory.volume) (hbound : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → |a z| ≤ 1) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → a z = 0) (hN : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator f) ≤ KP) : AEMeasurable (pastMultiplierSource a f) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) (pastMultiplierSource a f) ≤ KP

A cutoff of absolute value at most one preserves the pressure-gradient source exponent and its numerical bound.