Riesz Second All Exponents Paper

Supporting estimates for the Navier–Stokes development.

def CKN.Foundation.Euclidean.dualTruncSet (u : Parabolic.Vec3 → ℝ) (R : ℝ) : Set Parabolic.Vec3

The spatial and amplitude truncation used for dual exponent tests.

Equations

• CKN.Foundation.Euclidean.dualTruncSet u R = Metric.closedBall 0 R ∩ {x : CKN.Foundation.Parabolic.Vec3 | |u x| ≤ R}

noncomputable def CKN.Foundation.Euclidean.dualTruncField (u : Parabolic.Vec3 → ℝ) (p R : ℝ) : Parabolic.Vec3 → ℝ

The truncated dual-exponent test field for the real Riesz pairing.

Equations

• CKN.Foundation.Euclidean.dualTruncField u p R = (CKN.Foundation.Euclidean.dualTruncSet u R).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => |u x| ^ (p - 2) * u x

def CKN.Foundation.Euclidean.dualTruncENNSet (u : Parabolic.Vec3 → ℝ) (n : ℕ) : Set Parabolic.Vec3

The increasing spatial and amplitude truncations used in the ENNReal estimate.

Equations

• CKN.Foundation.Euclidean.dualTruncENNSet u n = CKN.Foundation.Euclidean.dualTruncSet u (↑n + 1)

noncomputable def CKN.Foundation.Euclidean.dualTruncENNPower (u : Parabolic.Vec3 → ℝ) (p : ℝ) (n : ℕ) : Parabolic.Vec3 → ENNReal

The truncated ENNReal power density used to pass to the full integral.

Equations

• CKN.Foundation.Euclidean.dualTruncENNPower u p n = (CKN.Foundation.Euclidean.dualTruncENNSet u n).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Euclidean.absE u x ^ p

noncomputable def CKN.Foundation.Euclidean.negativeRawExtensionInput {i j : Fin 3} {p : ENNReal} {C : ℝ} (hL2 : RieszSecondL2Input i j) (houtput : ∀ {f : Parabolic.Vec3 → ℝ}, MeasureTheory.MemLp f p MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp (-rieszSecondL2RawOperator hL2 f) p MeasureTheory.volume) (hbound : ∀ {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume), ‖MeasureTheory.MemLp.toLp (-rieszSecondL2RawOperator hL2 f) ⋯‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖) : LpExtensionInput p C

The extension input for the negative second Riesz transform.

Equations

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

theorem CKN.Foundation.Euclidean.riesz_second_all_exponents (s : ℝ) (hs : 1 < s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (i j : Fin 3), ∃ (T : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal s) MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal s) MeasureTheory.volume)), ‖T‖ ≤ C ∧ ∀ (g : Parabolic.Vec3 → ℝ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal s) MeasureTheory.volume), MeasureTheory.MemLp g 2 MeasureTheory.volume → (fun (x : Parabolic.Vec3) => ↑↑(T (MeasureTheory.MemLp.toLp g hg)) x) =ᵐ[MeasureTheory.volume] fun (x : Parabolic.Vec3) => -rieszSecondL2RawOperator (rieszSecondL2Input i j) g x

The concrete double Riesz transform has a bounded completed extension for every finite exponent strictly above one, agreeing with the negative raw L² operator on the common Lᵖ and L² domain.