Fixed-time endpoint pairing limits #
At a fixed time, the product of two cutoff-weighted spatial mollifications
converges in L¹ to the product of the two slices when the slices lie in
L∞ × L¹ or in L² × L². These are the fixed-time estimates behind the
endpoint density passage in lem:lps-comparison.
theorem
ESS.lps_lintegral_mul_le_two
{a b : CKN.Foundation.Parabolic.Vec3 → ℝ}
(ha : MeasureTheory.AEStronglyMeasurable a MeasureTheory.volume)
(hb : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume)
:
Cauchy–Schwarz for the spatial L¹ norm of a product.
theorem
ESS.lps_endpoint_slice_pairing_linf_l1
{f g : CKN.Foundation.Parabolic.Vec3 → ℝ}
{B : ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hB : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ B)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
:
(∀ (n : ℕ),
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖serrinCutoff n x * CKN.mollify f (serrinRadius n) ⋯ x * CKN.mollify g (serrinRadius n) ⋯ x - f x * g x‖ₑ ≤ 4 * ENNReal.ofReal B * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖g x‖ₑ) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖serrinCutoff n x * CKN.mollify f (serrinRadius n) ⋯ x * CKN.mollify g (serrinRadius n) ⋯ x - f x * g x‖ₑ)
Filter.atTop (nhds 0)
Fixed-time pairing limit for an essentially bounded factor and an
integrable factor: the cutoff-weighted product of mollifications converges in
L¹, with the error bounded by 4 B ‖g‖₁.
theorem
ESS.lps_endpoint_slice_pairing_l2_l2
{f g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
(∀ (n : ℕ),
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖serrinCutoff n x * CKN.mollify f (serrinRadius n) ⋯ x * CKN.mollify g (serrinRadius n) ⋯ x - f x * g x‖ₑ ≤ 6 * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume)) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖serrinCutoff n x * CKN.mollify f (serrinRadius n) ⋯ x * CKN.mollify g (serrinRadius n) ⋯ x - f x * g x‖ₑ)
Filter.atTop (nhds 0)
Fixed-time pairing limit for two square-integrable factors: the
cutoff-weighted product of mollifications converges in L¹, with the error
bounded by 6 ‖f‖₂ ‖g‖₂.