Past-time extension of a localized pressure field

Zero extension inside the past half-space preserves the localized source when its cutoff is supported in the smaller cylinder. No global weak-gradient characterization is asserted for the extended field.

noncomputable def CKN.Core.Endgame.causalPressureExtension (R : ℝ) (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Restrict a vector field to a cylinder in the past, retaining its future values.

Equations

• CKN.Core.Endgame.causalPressureExtension R Dp z = if z.2 ≤ 0 then (CKN.Foundation.Parabolic.parabolicCylinder 0 0 R).indicator Dp z else Dp z

theorem CKN.Core.Endgame.causalPressureExtension_eq_on_cylinder {R : ℝ} (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ Foundation.Parabolic.parabolicCylinder 0 0 R) : causalPressureExtension R Dp z = Dp z

The extension preserves the field on the smaller cylinder.

theorem CKN.Core.Endgame.causalPressureExtension_eq_on_future (R : ℝ) (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) {z : Foundation.Parabolic.ParabolicPoint} (hz : 0 < z.2) : causalPressureExtension R Dp z = Dp z

The extension preserves all future values.

theorem CKN.Core.Endgame.indicator_causalPressureExtension_component {R₁ R₀ : ℝ} (hR₁ : 0 ≤ R₁) (hR : R₁ ≤ R₀) (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (i : Fin 3) : ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => causalPressureExtension R₁ Dp z i) = (Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i

Indicating the extension on any larger cylinder gives exactly the original field indicated on the smaller cylinder, componentwise.

theorem CKN.Core.Endgame.causalPressureExtension_component_bounds {R₁ R₀ P τ : ℝ} {K : ENNReal} (hR₁ : 0 ≤ R₁) (hR : R₁ ≤ R₀) (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hAE : ∀ (i : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) MeasureTheory.volume) (hbound : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ K) (i : Fin 3) : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => causalPressureExtension R₁ Dp z i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => causalPressureExtension R₁ Dp z i) ≤ K

Both almost-everywhere measurability and every component Morrey bound transfer without changing the numerical bound.

theorem CKN.Core.Endgame.localizedGradientSourceG_causalPressureExtension (R : ℝ) (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 R) : Step4.localizedGradientSourceG φ u Du f (causalPressureExtension R Dp) = Step4.localizedGradientSourceG φ u Du f Dp

A cutoff whose past support lies in the smaller cylinder gives the same localized gradient-slot source after extension.