Time and space restrictions of measurable Riesz sources

A source restricted to a measurable spatial ball and time window has globally integrable slices almost everywhere when the original slices are integrable on that window. Its completed Riesz representative is selected on all times.

theorem CKN.Core.Step4.memLp_product_indicator_slices {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hB : MeasurableSet B) (hJ : MeasurableSet J) (hF : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : ∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => (B ×ˢ J).indicator F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Restriction to a product window turns restricted almost-everywhere slice integrability into a statement on the entire time axis.

theorem CKN.Core.Step4.exists_measurable_riesz_extension_field_on_window (j i : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} {x : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) {J : Set ℝ} (hJ : MeasurableSet J) (hF : AEMeasurable ((Foundation.Parabolic.vec3Ball x r ×ˢ J).indicator F) MeasureTheory.volume) (hFs : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, 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) => (Foundation.Parabolic.vec3Ball x r ×ˢ J).indicator F (y, s)

The completed Riesz operator of a ball-and-time restricted source admits one jointly measurable representative over the whole time axis.