Limits of weighted pairings #
Pairings ∫ c_n F_n G_n converge when F_n → F in L^p, G_n → G in the
conjugate L^q, and the weights are bounded by one and converge almost
everywhere; they tend to zero when the weights tend to zero uniformly. These
are the limit passages removing the mollification and cutoff in
lem:pv-serrin-uniqueness of the Escauriaza–Seregin–Šverák manuscript. Also
recorded: interpolation of L^p membership.
theorem
CKN.serrin_memLp_interpolate
{α : Type}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type}
[NormedAddCommGroup E]
{f : α → E}
{p q r : ENNReal}
(hp0 : p ≠ 0)
(hqtop : q ≠ ⊤)
(hpr : p ≤ r)
(hrq : r ≤ q)
(hfp : MeasureTheory.MemLp f p μ)
(hfq : MeasureTheory.MemLp f q μ)
:
MeasureTheory.MemLp f r μ
Membership in L^p and L^q gives membership in L^r for p ≤ r ≤ q.
theorem
CKN.serrin_weighted_pairing_tendsto
{α : Type}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
[hpq : p.HolderTriple q 1]
(hq : 1 ≤ q)
{F G c : α → ℝ}
{Fs Gs cs : ℕ → α → ℝ}
(hF : MeasureTheory.MemLp F p μ)
(hG : MeasureTheory.MemLp G q μ)
(hFs : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (Fs n) μ)
(hGs : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (Gs n) μ)
(hFlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => Fs n x - F x) p μ) Filter.atTop (nhds 0))
(hGlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => Gs n x - G x) q μ) Filter.atTop (nhds 0))
(hcm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (cs n) μ)
(hcb : ∀ (n : ℕ) (x : α), |cs n x| ≤ 1)
(hcm' : MeasureTheory.AEStronglyMeasurable c μ)
(hcb' : ∀ (x : α), |c x| ≤ 1)
(hc : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => cs n x) Filter.atTop (nhds (c x)))
:
Weighted pairings converge under L^p × L^q convergence of the factors
and almost everywhere convergence of weights bounded by one.
theorem
CKN.serrin_weighted_pairing_tendsto_zero
{α : Type}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
[hpq : p.HolderTriple q 1]
(hp : 1 ≤ p)
(hq : 1 ≤ q)
{F G : α → ℝ}
{Fs Gs cs : ℕ → α → ℝ}
(hF : MeasureTheory.MemLp F p μ)
(hG : MeasureTheory.MemLp G q μ)
(hFs : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (Fs n) μ)
(hGs : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (Gs n) μ)
(hFlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => Fs n x - F x) p μ) Filter.atTop (nhds 0))
(hGlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => Gs n x - G x) q μ) Filter.atTop (nhds 0))
{ε : ℕ → ℝ}
(hcb : ∀ (n : ℕ) (x : α), |cs n x| ≤ ε n)
(hε : Filter.Tendsto ε Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), cs n x * Fs n x * Gs n x ∂μ) Filter.atTop (nhds 0)
Weighted pairings tend to zero when the weights tend to zero uniformly and the factors converge in conjugate Lebesgue spaces.