Measurability of the fixed localized pressure sources #
The spatial mean is taken on the fixed localization ball. Both sources are restricted to the fixed time window and spatial ball before the completed operators are selected.
theorem
CKN.Core.Step4.fixed_pressure_sources_aemeasurable_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);
∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
V w i)
MeasureTheory.volume ∧ AEMeasurable
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
η w.1 * f w i)
MeasureTheory.volume
Suitability gives joint measurability of the localized force-free source and near-force source, including their time restriction.