Almost-everywhere measurability of one-sided localized fields #
The local measurability clauses of a suitable weak solution extend globally after multiplication by the indicator of the intermediate cylinder. A coefficient supported on a measurable set likewise localizes an a.e. measurable scalar field without requiring a global representative.
theorem
CKN.Core.Endgame.aemeasurable_mul_of_restrict_of_zero_outside
{S : Set Foundation.Parabolic.ParabolicPoint}
(hS : MeasurableSet S)
{a g : Foundation.Parabolic.ParabolicPoint → ℝ}
(ha : AEMeasurable a MeasureTheory.volume)
(hg : AEMeasurable g (MeasureTheory.volume.restrict S))
(hsupp : ∀ z ∉ S, a z = 0)
:
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => a z * g z) MeasureTheory.volume
A globally a.e. measurable coefficient supported on a measurable set turns a scalar field measurable only on that set into a globally a.e. measurable product.
theorem
CKN.Core.Endgame.one_sided_indicated_components_aemeasurable
{Ω : 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)
(hunit : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
:
(∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i)
MeasureTheory.volume) ∧ (∀ (i j : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i j)
MeasureTheory.volume) ∧ AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator p) MeasureTheory.volume ∧ ∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => f z i)
MeasureTheory.volume
Every component of the velocity, weak gradient, pressure, and force, indicated to the intermediate one-sided cylinder, is globally a.e. measurable. All measurability is supplied by the local solution clauses.