Jointly measurable representatives of the completed Riesz operator

The first potential is jointly measurable. Its spatial weak derivatives are the negatives of the completed Riesz operator, so measurable derivative selection gives representatives of that operator with the correct sign.

theorem CKN.Core.Step4.measurable_spacetime_newtonian_derivative_potential (j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Measurable F) : Measurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => F (y, z.2)) z.1

The first Newtonian derivative potential of jointly measurable data is jointly measurable in space and time.

theorem CKN.Core.Step4.exists_measurable_riesz_extension_field (j i : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Measurable F) (hFs : ∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => F (y, s)) : ∃ (T : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable T ∧ ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)

Compactly supported L^{6/5} slices admit one jointly measurable representative of the completed indexed Riesz operator, with equality on almost every spatial slice over the whole time axis.

theorem CKN.Core.Step4.exists_measurable_riesz_extension_field_of_aemeasurable (j i : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : AEMeasurable F MeasureTheory.volume) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hsupport : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), y ∉ K → F (y, s) = 0) (hFs : ∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : ∃ (T : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable T ∧ ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)

Almost-everywhere measurable sources with a fixed compact spatial support have jointly measurable completed Riesz representatives. The spatial support is imposed on the measurable source representative pointwise.