An integrable majorant for the paired commutator kernel #
Hölder's inequality with exponents 4/3 and 4 controls each kernel
section. Pairing the resulting uniform bound with an L¹ function also
proves integrability on the product space, so Fubini is applicable.
These results do not assume or construct a singular integral operator.
theorem
NavierStokesR3.PairedKernelBound.lpNorm_one_eq_integral_norm
{E : Type u_1}
[NormedAddCommGroup E]
{f : ProblemStatement.Space → E}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
:
The real L¹ comparison norm is the integral of the pointwise norm.
theorem
NavierStokesR3.PairedKernelBound.lpNorm_const_smul_of_nonneg
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ProblemStatement.Space → E}
{p : ENNReal}
{D : ℝ}
(hD : 0 ≤ D)
:
(Comparison.comparisonLpNorm p fun (x : ProblemStatement.Space) => D • f x) = D * Comparison.comparisonLpNorm p f
Nonnegative constant factors pass through the real comparison norm.
theorem
NavierStokesR3.PairedKernelBound.lpNorm_sub_left
{E : Type u_1}
[NormedAddCommGroup E]
{k : ProblemStatement.Space → E}
{p : ENNReal}
(hk : MeasureTheory.AEStronglyMeasurable k MeasureTheory.volume)
(x : ProblemStatement.Space)
:
(Comparison.comparisonLpNorm p fun (y : ProblemStatement.Space) => k (x - y)) = Comparison.comparisonLpNorm p k
A reflected translate has the same Lᵖ norm.
theorem
NavierStokesR3.PairedKernelBound.integrable_smul_and_integral_norm_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{k : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => k y • r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖k y • r y‖ ≤ Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
Hölder provides both integrability and the estimate for vector-valued data.
theorem
NavierStokesR3.PairedKernelBound.integrable_mul_and_integral_norm_le
{k r : ProblemStatement.Space → ℝ}
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => k y * r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖k y * r y‖ ≤ Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
The scalar multiplication estimate in ordinary real multiplication notation.
theorem
NavierStokesR3.PairedKernelBound.dominated_section_memLp_and_lpNorm_le
{m k : ProblemStatement.Space → ℝ}
(x : ProblemStatement.Space)
(hm : MeasureTheory.AEStronglyMeasurable m MeasureTheory.volume)
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hbound : ∀ᵐ (y : ProblemStatement.Space), ‖m y‖ ≤ k (x - y))
:
MeasureTheory.MemLp m (4 / 3) MeasureTheory.volume ∧ Comparison.comparisonLpNorm (4 / 3) m ≤ Comparison.comparisonLpNorm (4 / 3) k
A single measurable section can be dominated almost everywhere; no jointly measurable extension of that section is required.
theorem
NavierStokesR3.PairedKernelBound.dominated_section_integrable_and_integral_norm_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m k : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(x : ProblemStatement.Space)
(hm : MeasureTheory.AEStronglyMeasurable m MeasureTheory.volume)
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hbound : ∀ᵐ (y : ProblemStatement.Space), ‖m y‖ ≤ k (x - y))
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => m y • r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖m y • r y‖ ≤ Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
Hölder for one section dominated by a translated L^(4/3) majorant.
theorem
NavierStokesR3.PairedKernelBound.dominated_section_integrable_and_integral_norm_le_scaled
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m k : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
{D : ℝ}
(x : ProblemStatement.Space)
(hm : MeasureTheory.AEStronglyMeasurable m MeasureTheory.volume)
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hD : 0 ≤ D)
(hbound : ∀ᵐ (y : ProblemStatement.Space), ‖m y‖ ≤ D * k (x - y))
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => m y • r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖m y • r y‖ ≤ D * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
The single-section estimate with an explicit nonnegative constant.
theorem
NavierStokesR3.PairedKernelBound.section_memLp_and_lpNorm_le
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k : ProblemStatement.Space → ℝ}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
(x : ProblemStatement.Space)
:
MeasureTheory.MemLp (K x) (4 / 3) MeasureTheory.volume ∧ Comparison.comparisonLpNorm (4 / 3) (K x) ≤ Comparison.comparisonLpNorm (4 / 3) k
A measurable kernel section dominated by a reflected translate of an
L^(4/3) function has a uniform L^(4/3) bound.
theorem
NavierStokesR3.PairedKernelBound.section_integrable_and_integral_norm_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
(x : ProblemStatement.Space)
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => K x y • r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖K x y • r y‖ ≤ Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
Each paired section is genuinely Bochner integrable, with a bound independent of the outer variable.
theorem
NavierStokesR3.PairedKernelBound.section_integrable_and_integral_norm_le_scaled
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
{D : ℝ}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hD : 0 ≤ D)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ D * k (x - y))
(x : ProblemStatement.Space)
:
MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => K x y • r y) MeasureTheory.volume ∧ ∫ (y : ProblemStatement.Space), ‖K x y • r y‖ ≤ D * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
A scaled majorant gives the corresponding scaled uniform section bound.
theorem
NavierStokesR3.PairedKernelBound.integrable_paired_kernel
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
:
MeasureTheory.Integrable (fun (z : ProblemStatement.Space × ProblemStatement.Space) => g z.1 • K z.1 z.2 • r z.2)
(MeasureTheory.volume.prod MeasureTheory.volume)
Pairing with an L¹ function proves integrability on the whole product
space, not just existence of the iterated Bochner integral.
theorem
NavierStokesR3.PairedKernelBound.integrable_pairing
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
:
MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => g x • ∫ (y : ProblemStatement.Space), K x y • r y)
MeasureTheory.volume
The outer integral in the paired expression is integrable.
theorem
NavierStokesR3.PairedKernelBound.norm_paired_kernel_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
:
‖∫ (x : ProblemStatement.Space), g x • ∫ (y : ProblemStatement.Space), K x y • r y‖ ≤ Comparison.comparisonLpNorm 1 g * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
The paired kernel estimate for vector-valued data. In particular this applies to complex test functions through their real scalar action.
theorem
NavierStokesR3.PairedKernelBound.norm_paired_kernel_le_scaled
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
{D : ℝ}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hD : 0 ≤ D)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ D * k (x - y))
:
‖∫ (x : ProblemStatement.Space), g x • ∫ (y : ProblemStatement.Space), K x y • r y‖ ≤ D * Comparison.comparisonLpNorm 1 g * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
Explicit constants in the kernel bound pass through the pairing bound.
theorem
NavierStokesR3.PairedKernelBound.integral_pairing_swap
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : ProblemStatement.Space → ProblemStatement.Space → ℝ}
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hK : Measurable (Function.uncurry K))
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hbound : ∀ (x y : ProblemStatement.Space), ‖K x y‖ ≤ k (x - y))
:
∫ (x : ProblemStatement.Space), g x • ∫ (y : ProblemStatement.Space), K x y • r y = ∫ (y : ProblemStatement.Space) (x : ProblemStatement.Space), g x • K x y • r y
Fubini for the paired expression follows from actual product integrability.
theorem
NavierStokesR3.PairedKernelBound.norm_convolution_pairing_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{k g : ProblemStatement.Space → ℝ}
{r : ProblemStatement.Space → E}
(hkm : Measurable k)
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
:
‖∫ (x : ProblemStatement.Space), g x • ∫ (y : ProblemStatement.Space), k (x - y) • r y‖ ≤ Comparison.comparisonLpNorm 1 g * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
The direct convolution specialization needs only measurability of the
kernel and finite L^(4/3), L⁴, and L¹ norms.
theorem
NavierStokesR3.PairedKernelBound.abs_convolution_pairing_le
{k g r : ProblemStatement.Space → ℝ}
(hkm : Measurable k)
(hk : MeasureTheory.MemLp k (4 / 3) MeasureTheory.volume)
(hr : MeasureTheory.MemLp r 4 MeasureTheory.volume)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
:
|∫ (x : ProblemStatement.Space), g x * ∫ (y : ProblemStatement.Space), k (x - y) * r y| ≤ Comparison.comparisonLpNorm 1 g * Comparison.comparisonLpNorm (4 / 3) k * Comparison.comparisonLpNorm 4 r
The requested real-valued paired convolution inequality.