The radial majorant of the cutoff commutator

The cancellation factor min (‖z‖ / R) 1 makes the singular kernel belong to L^(4/3) in three dimensions. The proof uses the layer-cake formula and the volume of balls, so no principal-value integral occurs in this module.

noncomputable def NavierStokesR3.Comparison.radialCommutatorKernel (R : ℝ) (z : ProblemStatement.Space) : ℝ

The positive radial majorant after inserting the cutoff difference.

Equations

• NavierStokesR3.Comparison.radialCommutatorKernel R z = ‖z‖ ^ (-3) * min (‖z‖ / R) 1

theorem NavierStokesR3.Comparison.radialCommutatorKernel_nonneg {R : ℝ} (hR : 0 < R) (z : ProblemStatement.Space) : 0 ≤ radialCommutatorKernel R z

theorem NavierStokesR3.Comparison.radialCommutatorKernel_measurable (R : ℝ) : Measurable (radialCommutatorKernel R)

@[simp]

theorem NavierStokesR3.Comparison.radialCommutatorKernel_zero (R : ℝ) : radialCommutatorKernel R 0 = 0

theorem NavierStokesR3.Comparison.radialCommutatorKernel_scale {R : ℝ} (hR : 0 < R) (z : ProblemStatement.Space) : radialCommutatorKernel R z = R ^ (-3) * radialCommutatorKernel 1 (R⁻¹ • z)

Dilation of the cutoff kernel.

theorem NavierStokesR3.Comparison.radialCommutatorKernel_power_integrable {R : ℝ} (hR : 0 < R) : MeasureTheory.Integrable (fun (z : ProblemStatement.Space) => radialCommutatorKernel R z ^ (4 / 3)) MeasureTheory.volume

The 4/3 power of the radial kernel is integrable.

theorem NavierStokesR3.Comparison.radialCommutatorKernel_memLp {R : ℝ} (hR : 0 < R) : MeasureTheory.MemLp (radialCommutatorKernel R) (4 / 3) MeasureTheory.volume

The actual cancellation kernel belongs to L^(4/3).

theorem NavierStokesR3.Comparison.radialCommutatorKernel_lpNorm_scale {R : ℝ} (hR : 0 < R) : comparisonLpNorm (4 / 3) (radialCommutatorKernel R) = comparisonLpNorm (4 / 3) (radialCommutatorKernel 1) * R ^ (-(3 / 4))

The norm has exactly the scale required by the cutoff commutator.

theorem NavierStokesR3.Comparison.radialCommutatorKernel_lpNorm_le : ∃ (C : ℝ), 0 < C ∧ ∀ R > 0, comparisonLpNorm (4 / 3) (radialCommutatorKernel R) ≤ C * R ^ (-(3 / 4))

A single finite constant bounds the kernel norm at every positive radius.