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 initial velocity exponent supplies the linear velocity terms, while a cutoff of absolute value at most one preserves pressure-gradient bounds.

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

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

theorem CKN.Core.Endgame.bootstrap_pastMultiplierSource_aemeasurable {a f : Foundation.Parabolic.ParabolicPoint → ℝ} (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator f) MeasureTheory.volume) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16) → 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.bootstrap_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 (11 / 16) → a z = 0) : Foundation.Parabolic.Morrey.morreyNorm P τ (pastMultiplierSource a f) ≤ ENNReal.ofReal C * Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator f)

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

theorem CKN.Core.Endgame.bootstrap_causal_linear_velocity_source_morrey_le (C : ℝ) (KU : ENNReal) (hC : 0 ≤ C) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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 (11 / 16) → a z = 0) (hN : Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3) ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator f) ≤ KU) : AEMeasurable (pastMultiplierSource a f) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) (pastMultiplierSource a f) ≤ ENNReal.ofReal C * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KU)

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

theorem CKN.Core.Endgame.bootstrap_causal_linear_pressure_source_morrey_le (KP : ENNReal) (a f : Foundation.Parabolic.ParabolicPoint → ℝ) (ha : AEMeasurable a MeasureTheory.volume) (hf : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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 (11 / 16) → a z = 0) (hN : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator f) ≤ KP) : AEMeasurable (pastMultiplierSource a f) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) (pastMultiplierSource a f) ≤ KP

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