Weak convergence in Lp spaces

AbbreviationLebesgue measure on \((0,1)\)#✓fully proved

The measure on \(\mathbb{R}\) obtained by restricting Lebesgue measure to the open interval \((0, 1)\).

noncomputable abbrev μI01 : Measure ℝ := Measure.restrict volume (Set.Ioo (0 : ℝ) 1)

Used by 1

Used byBounded a.e.-null sequences in \(L^p(0,1)\) converge weakly to zero

TheoremBounded a.e.-null sequences in \(L^p(0,1)\) converge weakly to zero#●ready to prove

Let \(1 < p < \infty\) and let \(q\) be the conjugate exponent, so that \(1/p + 1/q = 1\). Write \(L^p(0,1)\) and \(L^q(0,1)\) for the Lebesgue spaces of real functions on \((0,1)\) with Lebesgue measure. Let \((f_n)_{n \in \mathbb{N}}\) be a sequence in \(L^p(0,1)\) with \(\|f_n\|_{L^p} \le 1\) for every \(n\) and \(f_n(x) \to 0\) for almost every \(x \in (0,1)\). Then for every \(g \in L^q(0,1)\),

\[ \int_0^1 f_n(x)\, g(x)\, dx \to 0 \quad (n \to \infty). \]

Since \(L^q(0,1)\) is the dual of \(L^p(0,1)\), this says that \((f_n)\) converges weakly to \(0\) in \(L^p(0,1)\).

public theorem_wanted tendsto_integral_mul_of_ae_tendsto_zero_of_eLpNorm_le_one
  (p q : ENNReal)
  (hp_ne_top : p ≠ ⊤)
  (hp_gt_one : 1 < p)
  (hq : 1 / p + 1 / q = 1)
  (f : ℕ → Lp ℝ p μI01)
  (h_bound : ∀ n, eLpNorm (f n) p μI01 ≤ 1)
  (h_ae : ∀ᵐ x ∂μI01, Tendsto (fun n => f n x) atTop (nhds 0)) :
  ∀ g : Lp ℝ q μI01, Tendsto (fun n => ∫ x, (f n x) * g x ∂μI01) atTop (nhds 0)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Normed linear spaces and Banach spaces; Banach lattices), problem ma_proofbench_l2_10.

Uses 1

Statement usesLebesgue measure on \((0,1)\)

TheoremWeak \(L^p\) limits of nonnegative functions are nonnegative#●ready to prove

Let \(1 < p < \infty\) and write \(L^p([0,1])\) for the Lebesgue space of real functions on \([0,1]\) with Lebesgue measure. Let \((f_n)_{n \in \mathbb{N}}\) be a sequence in \(L^p([0,1])\) such that for each \(n\), \(f_n(x) \ge 0\) for almost every \(x \in [0,1]\), and let \(f \in L^p([0,1])\). If \(f_n\) converges weakly to \(f\), that is, \(\ell(f_n) \to \ell(f)\) for every continuous linear functional \(\ell : L^p([0,1]) \to \mathbb{R}\), then \(f(x) \ge 0\) for almost every \(x \in [0,1]\).

public theorem_wanted ae_nonneg_of_weak_tendsto_of_ae_nonneg
    (p : ENNReal)
    [Fact (1 ≤ p)]
    (hp : 1 < p ∧ p < ⊤)
    (fn : ℕ → MeasureTheory.Lp ℝ p (Measure.restrict volume (Set.Icc (0 : ℝ) 1)))
    (f : MeasureTheory.Lp ℝ p (Measure.restrict volume (Set.Icc (0 : ℝ) 1)))
    (h_nonneg : ∀ n : ℕ, ∀ᵐ x ∂(Measure.restrict volume (Set.Icc (0 : ℝ) 1)), 0 ≤ fn n x)
    (hweak : ∀ l : (MeasureTheory.Lp ℝ p (Measure.restrict volume (Set.Icc (0 : ℝ) 1))) →L[ℝ] ℝ,
      Filter.Tendsto (fun n : ℕ => l (fn n)) Filter.atTop (nhds (l f))) :
    ∀ᵐ x ∂(Measure.restrict volume (Set.Icc (0 : ℝ) 1)), 0 ≤ f x

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Normed linear spaces and Banach spaces; Banach lattices), problem ma_proofbench_l2_16.

TheoremBounded almost everywhere convergent sequences in \(L^p\), \(1 < p < \infty\), converge weakly#●ready to prove

Bounded almost everywhere convergent sequences in \(L^p\), \(1 < p < \infty\), converge weakly. Let \(1 < p < \infty\) and let \(q\) be the conjugate exponent, \(1/p + 1/q = 1\). Let \(f\) and \(f_0, f_1, f_2, \dots\) be real-valued functions in \(L^p(\mathbb{R})\) such that \(f_n \to f\) almost everywhere and \(\sup_n \|f_n\|_{L^p} < \infty\). Then \(f_n\) converges weakly to \(f\): for every \(g \in L^q(\mathbb{R})\),

\[ \lim_{n\to\infty}\int_{\mathbb{R}} f_n g\,dx=\int_{\mathbb{R}} f g\,dx. \]

MathlibExt.MeasureTheory.WeakLpConvergenceOfAeConvergenceWanted.tendsto_integral_mul_of_ae_tendsto_of_eLpNorm_bounded · 17 lines

public theorem_wanted tendsto_integral_mul_of_ae_tendsto_of_eLpNorm_bounded
  (p q : ENNReal)
  (hp : 1 < p)
  (hp_top : p < ⊤)
  (hq : 1 / p + 1 / q = 1)
  (f : ℝ → ℝ)
  (fn : ℕ → ℝ → ℝ)
  (hfnLp : ∀ n : ℕ, MeasureTheory.MemLp (fn n) p MeasureTheory.volume)
  (hfLp : MeasureTheory.MemLp f p MeasureTheory.volume)
  (hae : ∀ᵐ x ∂MeasureTheory.volume, Filter.Tendsto (fun n : ℕ => fn n x) Filter.atTop (nhds (f x)))
  (hbound : ∃ M : ENNReal, M < ⊤ ∧ ∀ n : ℕ, MeasureTheory.eLpNorm (fn n) p MeasureTheory.volume ≤ M)
  (g : ℝ → ℝ)
  (hg : MeasureTheory.MemLp g q MeasureTheory.volume) :
  Filter.Tendsto
    (fun n : ℕ => ∫ x : ℝ, fn n x * g x)
    Filter.atTop
    (nhds (∫ x : ℝ, f x * g x))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Normed linear spaces and Banach spaces; Banach lattices), problem ma_proofbench_l2_82.

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.