Sliced convolution integrals and product-measure slicing

Two measure-theoretic facts used when a family of spatial statements indexed by time, such as the slice-wise pressure equation of lem:delta-p, is assembled into a single space-time statement.

• stronglyMeasurable_slice_kernel_integral: convolving a jointly measurable space-time integrand with a continuous kernel in the space variable alone produces a jointly measurable function of the space-time point.

• ae_ae_of_ae_prod_snd and ae_prod_of_ae_ae_snd: the two directions relating a product-almost-everywhere statement to its iterated form sliced in the second factor, which is the time factor in the product carrier Vec3 × ℝ. Mathlib states these for slices in the first factor; the versions here are obtained by transporting along the measure-preserving coordinate swap.

theorem CKN.stronglyMeasurable_slice_kernel_integral {d : ℕ} {K : Vec d → ℝ} (hK : Continuous K) {P : Vec d × ℝ → ℝ} (hP : MeasureTheory.StronglyMeasurable P) : MeasureTheory.StronglyMeasurable fun (z : Vec d × ℝ) => ∫ (y : Vec d), K y * P (z.1 - y, z.2)

A convolution-type integral against a continuous kernel, taken in the first factor only, is jointly measurable in both factors.

theorem CKN.ae_ae_of_ae_prod_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {p : α × β → Prop} (h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z) : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, p (x, y)

Slicing a product-almost-everywhere statement in the second factor.

theorem CKN.ae_prod_of_ae_ae_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, (x, y) ∈ s) : ∀ᵐ (z : α × β) ∂μ.prod ν, z ∈ s

Assembling a product-almost-everywhere membership from slices in the second factor.