Spatial slices of the space-time pressure #
The space-time pressure extension acts on almost every spatial slice by the
corresponding spatial Riesz operator (def:riesz-pressure).
noncomputable def
CKN.Leray.rieszPressureSpaceTimeComponentRepresentative
(r : ℝ)
(hr : 1 < r)
(i j : Fin 3)
:
A measurable representative of one space-time pressure component.
Equations
- CKN.Leray.rieszPressureSpaceTimeComponentRepresentative r hr i j u = AEMeasurable.mk ↑↑((CKN.Leray.rieszPressureSpaceTimeComponent r hr i j) u) ⋯
Instances For
theorem
CKN.Leray.rieszPressureSpaceTimeComponentRepresentative_measurable
(r : ℝ)
(hr : 1 < r)
(i j : Fin 3)
(u : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume))
:
Measurable (rieszPressureSpaceTimeComponentRepresentative r hr i j u)
The chosen space-time component representative is measurable.
theorem
CKN.Leray.rieszPressureSpaceTimeComponent_slice_ae_eq
(r : ℝ)
(hr : 1 < r)
(i j : Fin 3)
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.MemLp F (ENNReal.ofReal r) MeasureTheory.volume)
:
∀ᵐ (t : ℝ), ∃ (hFt :
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal r) MeasureTheory.volume),
(fun (x : Foundation.Parabolic.Vec3) =>
rieszPressureSpaceTimeComponentRepresentative r hr i j (MeasureTheory.MemLp.toLp F hF)
(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)) hFt))
x
The space-time double Riesz transform acts on almost every spatial slice as the spatial double Riesz transform, used by lem:pressure-split.
theorem
CKN.Leray.rieszPressureSpaceTime_slice_ae_eq
(r : ℝ)
(hr : 1 < r)
(F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume)
:
∀ᵐ (t : ℝ), ∃ (hFt :
∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) (ENNReal.ofReal r)
MeasureTheory.volume),
(fun (x : Foundation.Parabolic.Vec3) => rieszPressureSpaceTime r hr F hF (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : Foundation.Parabolic.Vec3) =>
↑↑(rieszPressureSlice r hr fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => F i j (y, t)) ⋯)
x
Almost every time slice of the space-time pressure is the spatial pressure of the corresponding tensor slice, used by lem:pressure-split.