Pressure Decay Measurability

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The pressure decomposition is evaluated on a bounded product cylinder. The solution fields have measurable representatives there; the representatives are used only to discharge the certificates needed by the eLpNorm' triangle inequality.

theorem CKN.Core.Step3.pressure_source_measurable_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) : ∃ (B : Set Foundation.Parabolic.Vec3) (T : Set ℝ) (η : Foundation.Parabolic.Vec3 → ℝ) (c : ℝ → Foundation.Parabolic.Vec3), B = Foundation.Parabolic.vec3Ball z.1 ρ ∧ T = Set.Ioc (z.2 - ρ ^ 2) z.2 ∧ η = mollifiedBallCutoff z.1 hρ ∧ (∀ (s : ℝ), c s = fun (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, s) j) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP1 η u c p f w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP2 η u c w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP3 η u c w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP4 η u c w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP5 η p w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP6 η p w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP7 η f w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)) ∧ MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP8 η f w.2 w.1) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ))