Pk Bounds P7 Solution Meas #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The HLS slice estimate is used on a product cylinder. This adapter keeps the representative used to witness the solution's a.e. measurability inside the proof; the public estimate therefore has no measurable-slice premise.
theorem
CKN.pressureP7_aestronglyMeasurable_on_cylinder
{Ω : 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)
:
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP7 (mollifiedBallCutoff z.1 hρ) f w.2 w.1)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ))