Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite-measure Lr includes into Lp for p<r

Statement

Let (X,A,μ) be a measure space with μ(X)<∞.

  1. If 1≤p<r<∞ and f∈Lr(μ), then f∈Lp(μ) and ∥f∥p≤μ(X)1/p−1/r∥f∥r.
  2. If 1≤p<∞ and f∈L∞(μ), then f∈Lp(μ) and ∥f∥p≤μ(X)1/p∥f∥∞.

Facts & Assumptions

Given: A finite measure space (X,A,μ).

[L1]

Holder's inequality for integrals is available (Holder's inequality for integrals, including the endpoint cases).

[L2]
[L3]
[L4]

If h∈L∞(μ), then ∣h∣≤∥h∥∞ almost everywhere (The essential supremum is attained as the least essential bound).

Proof

technique · Write $|f|^p$ as $|f|^p\cdot1$ and apply Holder with exponents $r/p$ and $r/(r-p)$. The finite total measure contributes the factor $\mu(X)^{1/p-1/r}$
1.1L1L2L3givenalgebra

Suppose 1≤p<r<∞ and put a:=rp,b:=rr−p. Then a,b∈(1,∞) and 1/a+1/b=1, so [L2] makes them conjugate. Apply [L1] to the functions ∣f∣p and 1: ∫∣f∣p dμ≤(∫∣f∣pa dμ)1/a(∫1b dμ)1/b=(∫∣f∣r dμ)p/rμ(X)1−p/r. Taking p-th roots gives the claimed bound.

1.2L3L4givenalgebra

If f∈L∞(μ), then ∫∣f∣p dμ≤∥f∥∞pμ(X). Indeed, ∣f∣p≤∥f∥∞p almost everywhere by [L4]. Thus f∈Lp(μ) and ∥f∥p≤μ(X)1/p∥f∥∞.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the finite-measure inclusion laws. [step 1.1, step 1.2].

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources