The concrete causal differentiated cutoff source

The paper source -2 ∂ⱼφ uᵢ, truncated to the past, is measurable using only local suitable-solution data. Its support and Morrey bound follow from the cutoff support, its derivative bound, and initial velocity norms.

noncomputable def CKN.Core.Endgame.causalDerivativeComponent (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (j i : Fin 3) : Foundation.Parabolic.ParabolicPoint → ℝ

A scalar component of the differentiated cutoff source in the past.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Endgame.causalDerivativeComponent_zero_outside_intermediate {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) (j i : Fin 3) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) : causalDerivativeComponent φ u j i z = 0

The causal differentiated source vanishes outside the intermediate cylinder, including at future times.

theorem CKN.Core.Endgame.causalDerivativeComponent_aemeasurable {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) (j i : Fin 3) (hu : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) MeasureTheory.volume) : AEMeasurable (causalDerivativeComponent φ u j i) MeasureTheory.volume

The causal differentiated source is globally measurable once the indicated velocity component is measurable. No global velocity assumption is required.

theorem CKN.Core.Endgame.causal_derivative_source_of_suitableWeakSolution (C : ℝ) (KU : ENNReal) (hC : 0 ≤ C) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hφ : φ ∈ spaceTimeTestFunction Ω I) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) (hder : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → ∀ (j : Fin 3), |spatialPartial φ j z| ≤ C) (hN : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) (j i : Fin 3) : AEMeasurable (causalDerivativeComponent φ u j i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) (causalDerivativeComponent φ u j i) ≤ ENNReal.ofReal (2 * C) * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KU)

The actual differentiated cutoff source inherits the initial velocity Morrey bound, with all coefficients fixed before the solution.