Spatial pressure operators

This file packages CKN's double Riesz transforms as the spatial operators used in def:riesz-pressure.

@[reducible, inline]

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

The nine spatial tensor components, used by def:riesz-pressure.

Equations

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

noncomputable def CKN.Leray.rieszPressureOperatorBound (r : ℝ) (hr : 1 < r) : ℝ

CKN's bound for one double Riesz transform, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureOperatorBound r hr = Classical.choose ⋯

noncomputable def CKN.Leray.rieszPressureOperator (r : ℝ) (hr : 1 < r) (i j : Fin 3) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

CKN's double Riesz transform at exponent r, used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureOperator r hr i j = Classical.choose ⋯

theorem CKN.Leray.rieszPressureOperator_norm_le (r : ℝ) (hr : 1 < r) (i j : Fin 3) : ‖rieszPressureOperator r hr i j‖ ≤ rieszPressureOperatorBound r hr

The chosen operator norm is bounded by the CKN constant, for def:riesz-pressure.

theorem CKN.Leray.rieszPressureOperator_ae_eq_negRaw (r : ℝ) (hr : 1 < r) (i j : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal r) MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) : (fun (x : Foundation.Parabolic.Vec3) => ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp g hg)) x) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => -Foundation.Euclidean.rieszSecondL2RawOperator (Foundation.Euclidean.rieszSecondL2Input i j) g x

The CKN all-exponent extension agrees with its signed L² definition on inputs in both spaces, as required by def:riesz-pressure.

theorem CKN.Leray.rieszPressureOperator_ae_eq_of_memLp_common (r : ℝ) (hr : 1 < r) (s : ℝ) (hs : 1 < s) (i j : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) (hgr : MeasureTheory.MemLp g (ENNReal.ofReal r) MeasureTheory.volume) (hgs : MeasureTheory.MemLp g (ENNReal.ofReal s) MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) : (fun (x : Foundation.Parabolic.Vec3) => ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp g hgr)) x) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ↑↑((rieszPressureOperator s hs i j) (MeasureTheory.MemLp.toLp g hgs)) x

The all-exponent operators coincide almost everywhere on the common L^r, L^s, and L² domain, as required by def:riesz-pressure.

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

The spatial pressure as the sum of the nine CKN double Riesz transforms, used by def:riesz-pressure.

Equations

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

theorem CKN.Leray.rieszPressureSlice_norm_le (r : ℝ) (hr : 1 < r) (F : PressureTensorLp r) : ‖rieszPressureSlice r hr F‖ ≤ rieszPressureOperatorBound r hr * ∑ i : Fin 3, ∑ j : Fin 3, ‖F i j‖

The spatial pressure bound by the sum of the component norms, used by def:riesz-pressure.

noncomputable def CKN.Leray.rieszPressureSliceRepresentative (r : ℝ) (hr : 1 < r) (F : PressureTensorLp r) : Foundation.Parabolic.Vec3 → ℝ

A measurable function representative of the spatial pressure used by def:riesz-pressure.

Equations

• CKN.Leray.rieszPressureSliceRepresentative r hr F = AEMeasurable.mk ↑↑(CKN.Leray.rieszPressureSlice r hr F) ⋯

theorem CKN.Leray.rieszPressureSliceRepresentative_ae_eq (r : ℝ) (hr : 1 < r) (F : PressureTensorLp r) : ↑↑(rieszPressureSlice r hr F) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative r hr F

The spatial pressure representative agrees almost everywhere with its L^r class, used by def:riesz-pressure.

theorem CKN.Leray.rieszPressureOperator_laplacian_pairing (r : ℝ) (hr : 1 < r) (i j : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) (hgr : MeasureTheory.MemLp g (ENNReal.ofReal r) MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp g hgr)) x * spatialLaplacian ψ x = -∫ (x : Foundation.Parabolic.Vec3), g x * mixedSecond ψ i j x

The signed distributional Laplacian identity for one tensor component, used by def:riesz-pressure.