Causality

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Causality of the heat potential

Step 3 of the proof of thm:A splits every localized source at t = 0, writing F = F⁻ + F⁺ and G_k = G_k⁻ + G_k⁺ with F⁻ = 1_{t ≤ 0} F, and observes that the positive-time kernel W₊ annihilates the future part, so that on {t ≤ 0} the localized velocity is the potential of the past part alone. heatPotential_time_truncation is that statement in the equivalent form used here: truncating the sources after a time does not change the potential at or before that time. No integrability hypothesis is needed, because the integrands agree pointwise, including at the boundary time. Consequently the cut-offs of Step 3 may reach {t > 0}, as they must, since the closure of the half cylinder contains its top face.

theorem CKN.Core.Endgame.time_truncation_source_data {F : Foundation.Parabolic.ParabolicPoint → ℝ} {P θ T : ℝ} (hP : 0 ≤ P) (hF : AEMeasurable F MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤) (hs : HasCompactSupport F) : AEMeasurable ({v : Foundation.Parabolic.ParabolicPoint | v.2 ≤ T}.indicator F) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm P θ ({v : Foundation.Parabolic.ParabolicPoint | v.2 ≤ T}.indicator F) < ⊤ ∧ HasCompactSupport ({v : Foundation.Parabolic.ParabolicPoint | v.2 ≤ T}.indicator F)

A time truncation preserves the data required by the heat-source estimate and cannot increase its Morrey seminorm.

theorem CKN.Core.Endgame.heatPotential_time_truncation (F : Foundation.Parabolic.ParabolicPoint → ℝ) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) {T : ℝ} {w : Foundation.Parabolic.ParabolicPoint} (hw : w.2 ≤ T) : HeatPotential.heatPotential ({v : Foundation.Parabolic.ParabolicPoint | v.2 ≤ T}.indicator F) (fun (i : Fin 3) => {v : Foundation.Parabolic.ParabolicPoint | v.2 ≤ T}.indicator (G i)) w = HeatPotential.heatPotential F G w

Truncating the sources after a time does not change their heat potential at or before that time. No integrability assumption is needed: the integrands are pointwise equal, including at the time boundary.