Lebesgue spaces

The spaces Lp of p-th power integrable functions: membership criteria, inclusions, dense subspaces, the essential supremum and weak convergence.

• Borel sets in Lp spaces
• Criteria for Lp membership
• Dense subspaces of Lp spaces
• Essential supremum
• Inclusions between Lp spaces
• Reverse Hölder inequality
• Weak convergence in Lp spaces

TheoremAn integral inequality for \(p\)-th powers with \(0 < p < 1\)#●ready to prove

Let \(\mu\) be a measure on a measurable space and let \(0 < p < 1\). Then for all real-valued \(f, g \in L^p(\mu)\),

\[\int \bigl||f|^p - |g|^p\bigr|\,d\mu \le \int |f - g|^p\,d\mu.\]

public theorem_wanted integral_abs_rpow_sub_rpow_le_integral_rpow_abs_sub
    {α : Type*} [MeasurableSpace α] {μ : Measure α} {p : ENNReal} (hp0 : 0 < p) (hp1 : p < 1)
    {f g : Lp ℝ p μ} :
    (∫ x, |((|f x|) ^ p.toReal) - ((|g x|) ^ p.toReal)| ∂μ) ≤
      ∫ x, (|f x - g x|) ^ p.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_53.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.