Completion of the space-time pressure operator

Compactly supported continuous fields form the dense core for the space-time extension in def:riesz-pressure.

theorem CKN.Leray.ae_eq_of_ae_time_sections {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : Measurable f) (hg : Measurable g) (h : ∀ᵐ (t : ℝ), (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => g (x, t)) : f =ᵐ[MeasureTheory.volume] g

Equality on almost every spatial time slice implies product almost-equality.

theorem CKN.Leray.ae_time_sections_of_ae_eq {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : Measurable f) (hg : Measurable g) (h : f =ᵐ[MeasureTheory.volume] g) : ∀ᵐ (t : ℝ), (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => g (x, t)

Product almost-equality gives almost-equality on almost every time slice.

noncomputable def CKN.Leray.rieszPressureComponentCompactRepresentative (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : Foundation.Parabolic.Vec3 × ℝ → ℝ

A measurable compact-input representative of the i,j space-time Riesz pressure component.

Equations

• CKN.Leray.rieszPressureComponentCompactRepresentative r hr i j hF hFc = Classical.choose ⋯

theorem CKN.Leray.rieszPressureComponentCompactRepresentative_memLp (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : MeasureTheory.MemLp (rieszPressureComponentCompactRepresentative r hr i j hF hFc) (ENNReal.ofReal r) MeasureTheory.volume

noncomputable def CKN.Leray.rieszPressureComponentCompactClass (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

The space-time L^r class of the compact slice representative, consumed by lem:riesz-duality.

Equations

• CKN.Leray.rieszPressureComponentCompactClass r hr i j hF hFc = MeasureTheory.MemLp.toLp (CKN.Leray.rieszPressureComponentCompactRepresentative r hr i j hF hFc) ⋯

theorem CKN.Leray.rieszPressureComponentCompactClass_add (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hG : Continuous G) (hFc : HasCompactSupport F) (hGc : HasCompactSupport G) : rieszPressureComponentCompactClass r hr i j ⋯ ⋯ = rieszPressureComponentCompactClass r hr i j hF hFc + rieszPressureComponentCompactClass r hr i j hG hGc

theorem CKN.Leray.rieszPressureComponentCompactClass_smul (r : ℝ) (hr : 1 < r) (i j : Fin 3) (c : ℝ) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : rieszPressureComponentCompactClass r hr i j ⋯ ⋯ = c • rieszPressureComponentCompactClass r hr i j hF hFc

theorem CKN.Leray.exists_rieszPressureComponentCompactClass_representative (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : ∃ (P : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable P ∧ MeasureTheory.MemLp P (ENNReal.ofReal r) MeasureTheory.volume ∧ P =ᵐ[MeasureTheory.volume] ↑↑(rieszPressureComponentCompactClass r hr i j hF hFc) ∧ ∀ᵐ (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

The compact-input pressure class has a measurable representative with the slice values used in def:riesz-pressure.

theorem CKN.Leray.hasCompactSupport_const_smul {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : HasCompactSupport F) (c : ℝ) : HasCompactSupport (c • F)

structure CKN.Leray.RieszPressureCompactInput : Type

A continuous compactly supported space-time scalar input, used as a dense core for def:riesz-pressure and lem:riesz-duality.

• value : Foundation.Parabolic.Vec3 × ℝ → ℝ

  The continuous compactly supported scalar function underlying a Riesz pressure input.

• continuous_value : Continuous self.value
• compact_support_value : HasCompactSupport self.value

def CKN.Leray.RieszPressureCompactInput.add (F G : RieszPressureCompactInput) : RieszPressureCompactInput

The pointwise sum of two compactly supported continuous pressure inputs.

Equations

• F.add G = { value := F.value + G.value, continuous_value := ⋯, compact_support_value := ⋯ }

def CKN.Leray.RieszPressureCompactInput.smul (c : ℝ) (F : RieszPressureCompactInput) : RieszPressureCompactInput

The scalar multiple of a compactly supported continuous pressure input.

Equations

• CKN.Leray.RieszPressureCompactInput.smul c F = { value := c • F.value, continuous_value := ⋯, compact_support_value := ⋯ }

noncomputable def CKN.Leray.rieszPressureCompactInputLpClass (r : ℝ) (_hr : 1 < r) (F : RieszPressureCompactInput) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

The L^r class of a compactly supported continuous input, used by the space-time pressure extension.

Equations

• CKN.Leray.rieszPressureCompactInputLpClass r _hr F = MeasureTheory.MemLp.toLp F.value ⋯

theorem CKN.Leray.rieszPressureCompactInputLpClass_add (r : ℝ) (hr : 1 < r) (F G : RieszPressureCompactInput) : rieszPressureCompactInputLpClass r hr (F.add G) = rieszPressureCompactInputLpClass r hr F + rieszPressureCompactInputLpClass r hr G

theorem CKN.Leray.rieszPressureCompactInputLpClass_smul (r : ℝ) (hr : 1 < r) (c : ℝ) (F : RieszPressureCompactInput) : rieszPressureCompactInputLpClass r hr (RieszPressureCompactInput.smul c F) = c • rieszPressureCompactInputLpClass r hr F

def CKN.Leray.rieszPressureSpaceTimeCore (r : ℝ) (hr : 1 < r) : Submodule ℝ ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

The submodule of L^r classes represented by continuous compactly supported inputs, used by lem:riesz-duality.

Equations

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

theorem CKN.Leray.rieszPressureSpaceTimeCore_dense (r : ℝ) (hr : 1 < r) : Dense {u : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume) | u ∈ rieszPressureSpaceTimeCore r hr}

The compact continuous input classes are dense in space-time L^r, used by def:riesz-pressure and lem:riesz-duality.

@[reducible, inline]

noncomputable abbrev CKN.Leray.RieszPressureSpaceTimeLp (r : ℝ) : AddSubgroup (Foundation.Parabolic.Vec3 × ℝ →ₘ[MeasureTheory.volume] ℝ)

The real-valued space-time L^r space used for pressure components.

Equations

• CKN.Leray.RieszPressureSpaceTimeLp r = MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume

@[reducible, inline]

abbrev CKN.Leray.RieszPressureSpaceTimeCore (r : ℝ) (hr : 1 < r) : Submodule ℝ ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)

The quotient-like core of compactly supported inputs for the space-time pressure operator at exponent r.

Equations

• CKN.Leray.RieszPressureSpaceTimeCore r hr = CKN.Leray.rieszPressureSpaceTimeCore r hr

noncomputable def CKN.Leray.rieszPressureSpaceTimeCoreComponentValue (r : ℝ) (hr : 1 < r) (i j : Fin 3) (u : ↥(RieszPressureSpaceTimeCore r hr)) : ↥(RieszPressureSpaceTimeLp r)

The L^r pressure component assigned to a compact-input equivalence class.

Equations

• CKN.Leray.rieszPressureSpaceTimeCoreComponentValue r hr i j u = CKN.Leray.rieszPressureComponentCompactClass r hr i j ⋯ ⋯

theorem CKN.Leray.rieszPressureSpaceTimeCoreComponentValue_eq (r : ℝ) (hr : 1 < r) (i j : Fin 3) (u : ↥(RieszPressureSpaceTimeCore r hr)) (F : RieszPressureCompactInput) (hF : ↑u = rieszPressureCompactInputLpClass r hr F) : rieszPressureSpaceTimeCoreComponentValue r hr i j u = rieszPressureComponentCompactClass r hr i j ⋯ ⋯

noncomputable def CKN.Leray.rieszPressureSpaceTimeCoreComponentMap (r : ℝ) (hr : 1 < r) (i j : Fin 3) : ↥(RieszPressureSpaceTimeCore r hr) →ₗ[ℝ] ↥(RieszPressureSpaceTimeLp r)

The linear map assigning the space-time Riesz pressure component to each compact-input class.

Equations

• CKN.Leray.rieszPressureSpaceTimeCoreComponentMap r hr i j = { toFun := CKN.Leray.rieszPressureSpaceTimeCoreComponentValue r hr i j, map_add' := ⋯, map_smul' := ⋯ }

theorem CKN.Leray.rieszPressureSpaceTimeCoreComponentMap_bound (r : ℝ) (hr : 1 < r) (i j : Fin 3) (u : ↥(RieszPressureSpaceTimeCore r hr)) : ‖(rieszPressureSpaceTimeCoreComponentMap r hr i j) u‖ ≤ rieszPressureOperatorBound r hr * ‖↑u‖

noncomputable def CKN.Leray.rieszPressureSpaceTimeComponent (r : ℝ) (hr : 1 < r) (i j : Fin 3) : ↥(RieszPressureSpaceTimeLp r) →L[ℝ] ↥(RieszPressureSpaceTimeLp r)

The space-time extension of one double Riesz transform, used by def:riesz-pressure and lem:riesz-duality.

Equations

• CKN.Leray.rieszPressureSpaceTimeComponent r hr i j = (CKN.Leray.rieszPressureSpaceTimeCoreComponentMap r hr i j).extendOfNorm ↑(CKN.Leray.rieszPressureSpaceTimeCore r hr).subtypeL

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

The space-time operator norm bound for one component, used by eq:riesz-spacetime-bound.

theorem CKN.Leray.rieszPressureSpaceTimeComponent_eq_compact (r : ℝ) (hr : 1 < r) (i j : Fin 3) {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) : (rieszPressureSpaceTimeComponent r hr i j) (MeasureTheory.MemLp.toLp F ⋯) = rieszPressureComponentCompactClass r hr i j hF hFc

On compactly supported continuous space-time inputs, the space-time extension is the joint representative constructed slice by slice, consumed by def:riesz-pressure.