The causal cutoff force term

Local force measurability on the unit cylinder suffices for the globally extended source, because the cutoff vanishes outside that cylinder in the past. Its numerical Morrey bound follows from the original small-data sum.

noncomputable def CKN.Core.Endgame.causalForceComponent (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (i : Fin 3) : Foundation.Parabolic.ParabolicPoint → ℝ

A scalar component of the cutoff force, extended by zero to future times.

Equations

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

theorem CKN.Core.Endgame.causalForceComponent_zero_outside_unit {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → φ z = 0) (i : Fin 3) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1) : causalForceComponent φ f i z = 0

The causal force component vanishes outside the unit cylinder.

theorem CKN.Core.Endgame.causalForceComponent_aemeasurable {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hφ : AEMeasurable φ MeasureTheory.volume) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → φ z = 0) (i : Fin 3) (hf : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 1))) : AEMeasurable (causalForceComponent φ f i) MeasureTheory.volume

Global measurability of the causal force uses only local measurability of the original force on the unit cylinder.

theorem CKN.Core.Endgame.abs_causalForceComponent_le {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hφ : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → 0 ≤ φ z ∧ φ z ≤ 1) (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : |causalForceComponent φ f i z| ≤ Foundation.Parabolic.vec3EuclideanNorm (f z)

A cutoff taking values in [0,1] in the past yields pointwise force domination, including after extension by zero.

theorem CKN.Core.Endgame.causalForceComponent_paper_morrey_le (q ε₀ : ℝ) (hq : 5 / 2 < q) {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : AEMeasurable φ MeasureTheory.volume) (hφrange : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → 0 ≤ φ z ∧ φ z ≤ 1) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → φ z = 0) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (i : Fin 3) (hf : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 1))) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) (causalForceComponent φ f i) ≤ forceSourceMorreyBound q ε₀

The concrete causal cutoff force component satisfies the uniform paper source Morrey bound.

theorem CKN.Core.Endgame.causal_force_source_of_suitableWeakSolution (q ε₀ : ℝ) (hq : 5 / 2 < q) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {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φ : AEMeasurable φ MeasureTheory.volume) (hφrange : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → 0 ≤ φ z ∧ φ z ≤ 1) (hsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → φ z = 0) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (i : Fin 3) : AEMeasurable (causalForceComponent φ f i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) (causalForceComponent φ f i) ≤ forceSourceMorreyBound q ε₀

Suitable-solution local energy data supply all force measurability needed for the concrete causal source estimate.