Joint pressure representatives for compactly supported space-time data

The completed CKN operator supplies jointly measurable representatives on compactly supported spatial slices. This file identifies those representatives with the all-exponent ESS pressure on common-domain slices.

theorem CKN.Leray.continuous_spaceTimeSlice_hasCompactSupport {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hFc : HasCompactSupport F) (t : ℝ) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => F (x, t)

Spatial slices of a compactly supported space-time function retain compact support, used by def:riesz-pressure.

theorem CKN.Leray.eLpNorm_spaceTime_pow_eq_integral_slice (r : ℝ) (hr : 0 < r) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.AEStronglyMeasurable F MeasureTheory.volume) : MeasureTheory.eLpNorm F (ENNReal.ofReal r) MeasureTheory.volume ^ r = ∫⁻ (t : ℝ), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal r) MeasureTheory.volume ^ r

Tonelli's formula for the (r)-power of a space-time (L^r) seminorm, used by eq:riesz-spacetime-bound.

theorem CKN.Leray.exists_measurable_rieszPressure_component_of_compact (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : ∃ (P : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable P ∧ ∀ᵐ (t : ℝ), (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => F (y, t)) ⋯)) x

A continuous compactly supported space-time input has a jointly measurable representative of its signed double Riesz transform, used by def:riesz-pressure.

theorem CKN.Leray.exists_rieszPressure_component_memLp_bound_of_compact (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : ∃ (P : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable P ∧ (∀ᵐ (t : ℝ), (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => F (y, t)) ⋯)) x) ∧ MeasureTheory.MemLp P (ENNReal.ofReal r) MeasureTheory.volume ∧ MeasureTheory.eLpNorm P (ENNReal.ofReal r) MeasureTheory.volume ≤ ENNReal.ofReal (rieszPressureOperatorBound r hr) * MeasureTheory.eLpNorm F (ENNReal.ofReal r) MeasureTheory.volume

The joint component representative for compact data is in product-space L^r, with the componentwise CKN bound; used by eq:riesz-spacetime-bound.