Inclusions between Lp spaces

TheoremA bounded integrable function is square integrable#●ready to prove

Let \(d\) be a natural number, let \(M \ge 0\), and let \(f \colon \mathbb{R}^d \to \mathbb{R}\) satisfy \(|f(x)| \le M\) for every \(x \in \mathbb{R}^d\). If \(f \in L^1(\mathbb{R}^d)\), then \(f \in L^2(\mathbb{R}^d)\) and

\[\|f\|_{L^2(\mathbb{R}^d)} \le M^{1/2} \, \|f\|_{L^1(\mathbb{R}^d)}^{1/2},\]

where the spaces and norms are taken with respect to Lebesgue measure.

public theorem_wanted memLp_two_and_eLpNorm_two_le_of_bounded_of_memLp_one
    (d : ℕ) (f : (Fin d → ℝ) → ℝ) (M : ℝ) (hM : 0 ≤ M) (hbound : ∀ x, ‖f x‖ ≤ M)
    (hf : MeasureTheory.MemLp f 1) :
    (MeasureTheory.MemLp f 2) ∧
      (MeasureTheory.eLpNorm f 2).toReal ≤
        Real.sqrt M * Real.sqrt (MeasureTheory.eLpNorm f 1).toReal

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l1_41.

Theorem\(L^1(\mathbb{R}^d)\) and \(L^2(\mathbb{R}^d)\) are incomparable#●ready to prove

Let \(d \ge 1\). With respect to Lebesgue measure on \(\mathbb{R}^d\), there is a function \(f : \mathbb{R}^d \to \mathbb{R}\) in \(L^2(\mathbb{R}^d)\) that is not in \(L^1(\mathbb{R}^d)\), and there is a function \(g : \mathbb{R}^d \to \mathbb{R}\) in \(L^1(\mathbb{R}^d)\) that is not in \(L^2(\mathbb{R}^d)\).

public theorem_wanted not_memLp_two_subset_one_and_not_memLp_one_subset_two (d : ℕ) (hd : 0 < d) :
    (¬ (∀ f : (Fin d → ℝ) → ℝ,
        MeasureTheory.MemLp f 2 →
        MeasureTheory.MemLp f 1)) ∧
    (¬ (∀ f : (Fin d → ℝ) → ℝ,
        MeasureTheory.MemLp f 1 →
        MeasureTheory.MemLp f 2))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l1_97.

TheoremAn \(L^p\) function with finite \(L^q\) mass on finite-measure sets is in \(L^q\)#●ready to prove

Let \(1 \le p < q < \infty\) and let \(f : \mathbb{R} \to \mathbb{R}\) belong to \(L^p(\mathbb{R})\). If \(\int_A |f|^q < \infty\) for every Borel set \(A \subseteq \mathbb{R}\) of finite Lebesgue measure, then \(f \in L^q(\mathbb{R})\).

public theorem_wanted memLp_of_memLp_of_lintegral_rpow_lt_top_of_measure_lt_top
    {p q : ENNReal}
    (hp : 1 ≤ p) (hpq : p < q) (hq : q < ⊤)
    (f : ℝ → ℝ)
    (hfLp : MeasureTheory.MemLp f p MeasureTheory.volume)
    (hA : ∀ A : Set ℝ, MeasurableSet A → MeasureTheory.volume A < ⊤ →
      (∫⁻ x in A, (ENNReal.ofReal |f x|) ^ q.toReal ∂MeasureTheory.volume) < ⊤) :
    MeasureTheory.MemLp f q MeasureTheory.volume

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_24.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.