Jointly measurable completed pressure operators from suitability #
Both force-free and near-force sources use one spatial cutoff and one time window. The selected operator fields satisfy the completed-operator identity on the full spatial space at almost every time, including the zero extension.
theorem
CKN.Core.Step4.exists_measurable_fixed_riesz_fields_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
have η := mollifiedBallCutoff z.1 hρ;
have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du (sourceSliceCentredMean z.1 ρ u);
have Q := Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ;
∃ (T : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (Tforce :
Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ),
(∀ (j i : Fin 3), Measurable (T j i)) ∧ (∀ (j i : Fin 3), Measurable (Tforce j i)) ∧ (∀ (j i : Fin 3),
∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j i (y, s)) =ᵐ[MeasureTheory.volume]
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
fun (y : Foundation.Parabolic.Vec3) =>
Q.indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => V w j) (y, s)) ∧ ∀ (j i : Fin 3),
∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => Tforce j i (y, s)) =ᵐ[MeasureTheory.volume]
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
fun (y : Foundation.Parabolic.Vec3) =>
Q.indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => η w.1 * f w j) (y, s)
Suitable-solution data give jointly measurable completed Riesz fields for both fixed sources, with the spatial and time indicators explicit.
theorem
CKN.Core.Step4.product_indicator_slice_eq_of_support
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{s : ℝ}
(hs : s ∈ J)
(hF : ∀ y ∉ B, F (y, s) = 0)
:
On the chosen time window, spatial restriction does not change a source that vanishes off the localization ball.
theorem
CKN.Core.Step4.fixed_centred_source_eq_zero_off_ball
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(y : Foundation.Parabolic.Vec3)
(s : ℝ)
(i : Fin 3)
(hy : y ∉ Foundation.Parabolic.vec3Ball x ρ)
:
sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff x hρ) (spatialDeriv (mollifiedBallCutoff x hρ)) u Du c
(y, s) i = 0
The fixed force-free source vanishes pointwise outside its cutoff ball.
theorem
CKN.Core.Step4.fixed_pressure_sources_indicator_slice_eq
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{ρ s : ℝ}
(hρ : 0 < ρ)
(hs : s ∈ Set.Ioc (z.2 - ρ ^ 2) z.2)
(j : Fin 3)
:
have η := mollifiedBallCutoff z.1 hρ;
have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du (sourceSliceCentredMean z.1 ρ u);
((fun (y : Foundation.Parabolic.Vec3) =>
(Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) => V w j) (y, s)) = fun (y : Foundation.Parabolic.Vec3) => V (y, s) j) ∧ (fun (y : Foundation.Parabolic.Vec3) =>
(Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) => η w.1 * f w j) (y, s)) = fun (y : Vec 3) => η y * f (y, s) j
On each time in the localization window, the spatial cutoff makes both indicator-restricted sources equal to the original localized sources.