Criteria for Lp membership

TheoremLebesgue integrals over truncations of a set#✓fully proved

Let \(\lambda\) be Lebesgue measure on \(\mathbb{R}\), let \(S \subseteq \mathbb{R}\) be measurable, and let \(g : \mathbb{R} \to [0, \infty]\) be measurable. Then

\[\int_S g \, d\lambda = \sup_{n \in \mathbb{N}} \int_{[-n, n] \cap S} g \, d\lambda.\]

This is monotone convergence applied to the indicators of the truncations.

theorem lintegral_eq_iSup_lintegral_Icc_inter
    (S : Set ℝ) (hS : MeasurableSet S) (g : ℝ → ℝ≥0∞) (hg : Measurable g) :
    ∫⁻ x in S, g x ∂volume =
      ⨆ n : ℕ, ∫⁻ x in (Set.Icc (-(n : ℝ)) n) ∩ S, g x ∂volume

Used by 1

Used byCharacterization of \(L^p\) membership via truncated integrals

TheoremCharacterization of \(L^p\) membership via truncated integrals#✓fully proved

Let \(\lambda\) be Lebesgue measure on \(\mathbb{R}\), let \(F\) be a second-countable normed additive commutative group with its Borel \(\sigma\)-algebra, let \(0 < p < \infty\), let \(S \subseteq \mathbb{R}\) be measurable, and let \(f : \mathbb{R} \to F\) be measurable. Then \(f\) belongs to \(L^p\) of \(\lambda\) restricted to \(S\) if and only if

\[\sup_{n \in \mathbb{N}} \int_{[-n, n] \cap S} \|f(x)\|^p \, d\lambda(x) < \infty,\]

where the integrals are taken in \([0, \infty]\).

theorem memLp_iff_iSup_lintegral_Icc_inter_lt_top
    {F : Type*} [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F]
    [SecondCountableTopology F]
    {p : ℝ≥0∞} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤)
    (S : Set ℝ) (hS : MeasurableSet S) {f : ℝ → F} (hf : Measurable f) :
    MemLp f p (volume.restrict S) ↔
      ⨆ n : ℕ, ∫⁻ x in (Set.Icc (-(n : ℝ)) n) ∩ S, (‖f x‖ₑ) ^ p.toReal ∂volume < ⊤

Uses 1

Proof usesLebesgue integrals over truncations of a set

TheoremPolynomial decay implies \(L^p\) membership#✓fully proved

Let \(E\) be a normed additive commutative group and let \(f : \mathbb{R} \to E\) be almost everywhere strongly measurable. Suppose there are real numbers \(C \ge 0\) and \(q > 1\) such that \(\|f(x)\| \le C (1 + |x|)^{-q}\) for almost every \(x \in \mathbb{R}\). Then \(f \in L^p(\mathbb{R})\), with respect to Lebesgue measure, for every \(p \in [1, \infty]\).

theorem memLp_of_polynomial_decay_ae
    {E : Type*} [NormedAddCommGroup E]
    {f : ℝ → E} (hf_meas : AEStronglyMeasurable f volume)
    {C : ℝ} (hC : 0 ≤ C) {q : ℝ} (hq : 1 < q)
    (hbound : ∀ᵐ x : ℝ ∂volume, ‖f x‖ ≤ C * (1 + |x|) ^ (-q))
    {p : ℝ≥0∞} (hp : 1 ≤ p) :
    MemLp f p volume

Used by 1

Used byPointwise polynomial decay implies \(L^p\) membership

TheoremPointwise polynomial decay implies \(L^p\) membership#✓fully proved

Let \(E\) be a normed additive commutative group and let \(f : \mathbb{R} \to E\) be almost everywhere strongly measurable. Suppose there are real numbers \(C \ge 0\) and \(q > 1\) such that \(\|f(x)\| \le C (1 + |x|)^{-q}\) for every \(x \in \mathbb{R}\). Then \(f \in L^p(\mathbb{R})\), with respect to Lebesgue measure, for every \(p \in [1, \infty]\).

theorem memLp_of_polynomial_decay
    {E : Type*} [NormedAddCommGroup E]
    {f : ℝ → E} (hf_meas : AEStronglyMeasurable f volume)
    {C : ℝ} (hC : 0 ≤ C) {q : ℝ} (hq : 1 < q)
    (hbound : ∀ x : ℝ, ‖f x‖ ≤ C * (1 + |x|) ^ (-q))
    {p : ℝ≥0∞} (hp : 1 ≤ p) :
    MemLp f p volume

Uses 1

Proof usesPolynomial decay implies \(L^p\) membership

DefinitionPartitions of the unit interval#✓fully proved

For a natural number \(n\), real numbers \(t_0, t_1, \dots, t_n\) form a partition of \([0, 1]\) when \(0 = t_0 < t_1 < \dots < t_n = 1\).

def IsPartition01 {n : ℕ} (t : Fin (n + 1) → ℝ) : Prop :=
  t 0 = 0 ∧ t (Fin.last n) = 1 ∧ StrictMono t

Used by 1

Used by\(L^p\) on \((0,1)\) via averages over partitions

DefinitionPartition average sum#✓fully proved

For a function \(f : \mathbb{R} \to \mathbb{R}\), a real number \(p\) and real numbers \(t_0, t_1, \dots, t_n\), the partition average sum is

\[\sum_{i=0}^{n-1} (t_{i+1} - t_i) \left(\frac{1}{t_{i+1} - t_i} \int_{[t_i, t_{i+1}]} |f(x)|\,dx\right)^p,\]

where the integrals are Lebesgue integrals over the closed intervals \([t_i, t_{i+1}]\) (empty when \(t_{i+1} < t_i\)), the integral of a function that is not integrable there counts as \(0\), \(1/0 = 0\), and \(0^p\) is taken to be \(1\) when \(p = 0\) and \(0\) when \(p \ne 0\).

def partitionAverageSum (f : ℝ → ℝ) (p : ℝ) {n : ℕ} (t : Fin (n + 1) → ℝ) : ℝ :=
  ∑ i : Fin n,
    let a := t i.castSucc
    let b := t i.succ
    (b - a) * Real.rpow ((1 / (b - a)) * ∫ x in Set.Icc a b, |f x|) p

Used by 1

Used by\(L^p\) on \((0,1)\) via averages over partitions

Theorem\(L^p\) on \((0,1)\) via averages over partitions#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be in \(L^1([0, 1])\) and let \(p > 1\) be a real number. Then \(f \in L^p([0, 1])\) if and only if there is a real number \(C\) such that

\[\sum_{i=0}^{n-1} (t_{i+1} - t_i) \left(\frac{1}{t_{i+1} - t_i} \int_{t_i}^{t_{i+1}} |f(x)|\,dx\right)^p \le C\]

for every partition \(0 = t_0 < t_1 < \dots < t_n = 1\) of \([0, 1]\). Here \(L^1([0, 1])\) and \(L^p([0, 1])\) are taken with respect to Lebesgue measure restricted to \([0, 1]\).

public theorem_wanted memLp_iff_bddAbove_partitionAverageSum
    (f : ℝ → ℝ) (p : ℝ)
    (hp : 1 < p)
    (hf_L1 : MemLp f 1 (volume.restrict (Set.Icc (0 : ℝ) 1))) :
    MemLp f (ENNReal.ofReal p) (volume.restrict (Set.Icc (0 : ℝ) 1)) ↔
      ∃ C : ℝ, ∀ n : ℕ, ∀ t : Fin (n + 1) → ℝ,
        IsPartition01 t →
          partitionAverageSum f p t ≤ C

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_02.

Uses 2

Statement usesPartitions of the unit interval · Partition average sum

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.