Space-time pressure on L^r

This file sums the nine bounded component operators and chooses a measurable representative of their space-time pressure.

@[reducible, inline]

abbrev CKN.Leray.RieszPressureSpaceTimeTensorLp (r : ℝ) : Type

A tensor of space-time L^r classes, used by def:riesz-pressure.

Equations

• CKN.Leray.RieszPressureSpaceTimeTensorLp r = (Fin 3 → Fin 3 → ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume))

noncomputable def CKN.Leray.rieszPressureSpaceTimeClass (r : ℝ) (hr : 1 < r) (F : RieszPressureSpaceTimeTensorLp r) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

The space-time pressure class formed from the nine double Riesz transforms, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureSpaceTimeClass r hr F = ∑ i : Fin 3, ∑ j : Fin 3, (CKN.Leray.rieszPressureSpaceTimeComponent r hr i j) (F i j)

noncomputable def CKN.Leray.rieszPressureSpaceTimeRepresentative (r : ℝ) (hr : 1 < r) (F : RieszPressureSpaceTimeTensorLp r) : Foundation.Parabolic.Vec3 × ℝ → ℝ

A jointly measurable representative of the space-time pressure class, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureSpaceTimeRepresentative r hr F = AEMeasurable.mk ↑↑(CKN.Leray.rieszPressureSpaceTimeClass r hr F) ⋯

theorem CKN.Leray.rieszPressureSpaceTimeRepresentative_measurable (r : ℝ) (hr : 1 < r) (F : RieszPressureSpaceTimeTensorLp r) : Measurable (rieszPressureSpaceTimeRepresentative r hr F)

The representative selected for space-time pressure is measurable, used by def:riesz-pressure.

theorem CKN.Leray.rieszPressureSpaceTimeRepresentative_memLp (r : ℝ) (hr : 1 < r) (F : RieszPressureSpaceTimeTensorLp r) : MeasureTheory.MemLp (rieszPressureSpaceTimeRepresentative r hr F) (ENNReal.ofReal r) MeasureTheory.volume

The space-time pressure representative belongs to L^r, used by def:riesz-pressure.

theorem CKN.Leray.rieszPressureSpaceTimeClass_norm_le (r : ℝ) (hr : 1 < r) (F : RieszPressureSpaceTimeTensorLp r) : ‖rieszPressureSpaceTimeClass r hr F‖ ≤ rieszPressureOperatorBound r hr * ∑ i : Fin 3, ∑ j : Fin 3, ‖F i j‖

The nine component bounds give the space-time L^r bound, used by eq:riesz-spacetime-bound.

noncomputable def CKN.Leray.rieszPressureSpaceTimeTensorToLp (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) : RieszPressureSpaceTimeTensorLp r

Convert a jointly measurable tensor with L^r space-time components to its canonical tensor of L^r classes, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureSpaceTimeTensorToLp r _hr F hF i j = MeasureTheory.MemLp.toLp (F i j) ⋯

theorem CKN.Leray.rieszPressureSpaceTime_bound (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) : ‖rieszPressureSpaceTimeClass r hr (rieszPressureSpaceTimeTensorToLp r hr F hF)‖ ≤ rieszPressureOperatorBound r hr * ∑ i : Fin 3, ∑ j : Fin 3, ‖MeasureTheory.MemLp.toLp (F i j) ⋯‖

For a raw tensor with space-time L^r components, the pressure class obeys eq:riesz-spacetime-bound in the corresponding L^r norms.

noncomputable def CKN.Leray.rieszPressureSpaceTime (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) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The jointly measurable pressure associated with a tensor whose components belong to space-time L^r, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureSpaceTime r hr F hF = CKN.Leray.rieszPressureSpaceTimeRepresentative r hr (CKN.Leray.rieszPressureSpaceTimeTensorToLp r hr F hF)

theorem CKN.Leray.rieszPressureSpaceTime_measurable (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) : Measurable (rieszPressureSpaceTime r hr F hF)

The function-valued space-time pressure is measurable, used by def:riesz-pressure.

theorem CKN.Leray.rieszPressureSpaceTime_memLp (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) : MeasureTheory.MemLp (rieszPressureSpaceTime r hr F hF) (ENNReal.ofReal r) MeasureTheory.volume

The function-valued space-time pressure belongs to L^r, used by def:riesz-pressure.