Space-time Riesz pressure duality

The pressure operators are paired through the integral on the product space.

theorem CKN.Leray.rieszPressureLpPairing_bound (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (u : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)) (v : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) : ‖∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑u z * ↑↑v z‖ ≤ ‖u‖ * ‖v‖

noncomputable def CKN.Leray.rieszPressureLpPairingLinear (r q : ℝ) (hHolder : r.HolderConjugate q) (v : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume) →ₗ[ℝ] ℝ

The linear pairing of an L^r field with a fixed conjugate L^q field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.rieszPressureLpPairingCLM (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (v : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume) →L[ℝ] ℝ

The Hölder pairing as a continuous functional, used by lem:riesz-duality.

Equations

• CKN.Leray.rieszPressureLpPairingCLM r hr q hq hHolder v = (CKN.Leray.rieszPressureLpPairingLinear r q hHolder v).mkContinuous ‖v‖ ⋯

theorem CKN.Leray.rieszPressureLpPairingCLM_apply (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (v : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) (u : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)) : (rieszPressureLpPairingCLM r hr q hq hHolder v) u = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑u z * ↑↑v z

Evaluation of rieszPressureLpPairingCLM, used by lem:riesz-duality.