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.

Generalized Holder inequality puts products into Lr

Statement

Let 1p,q,r satisfy

1r=1p+1q,

with the convention 1/=0. If f and g lie in the corresponding measurable-function spaces (Lp(μ) or L(μ) according to whether the exponent is finite or infinite), then fg lies in the corresponding space for r and

fgrfpgq.

Facts & Assumptions

Given: Exponents p,q,r with 1/r=1/p+1/q and measurable functions f,g in the spaces named in the Statement.

[L1]

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

[L2]

Conjugate exponents include the endpoint convention 1/=0 (Conjugate exponents, including the endpoint conventions).

[L3]

For 0<s<, hLs(μ) means hsdμ<, and L(μ) means finite essential supremum (The function space Lp(μ) for 0<p<, The space L(μ) of essentially bounded measurable functions).

[L4]

If hL(μ), then hh almost everywhere (The essential supremum is attained as the least essential bound).

Proof

Proof technique: Raise fg to the r-th power and apply Holder to fr and gr with conjugate exponents p/r and q/r.

1.1

If r=, then 1/p=1/q=0, so p=q= by [L2]. Hence [L2, L3, L4, given] fgfg almost everywhere, and taking essential suprema gives fgfg.

1.2

If p= and r<, then q=r. The pointwise bound and the definition of gr give [L2, L3, L4, given] fgrrfrgrr. Indeed, [L4] gives ff almost everywhere, so fgrfrgr almost everywhere. Taking r-th roots yields the claim. The case q= is symmetric.

1.3

Assume now that r< and p,q<. Then [L1, L2, L3, given, algebra] 1=rp+rq, so the exponents p/r and q/r are conjugate. Because frLp/r(μ) and grLq/r(μ), [L1] applied to these two functions gives fgrdμ(fpdμ)r/p(gqdμ)r/q=fprgqr.

2.1

Step 1.1 covers r=, step 1.2 covers the one-infinite endpoint cases, and step 1.3 covers the fully finite case. [step 1.1, step 1.2, step 1.3] In each case fgrfpgq, so fg lies in the stated r-space. ∎

Depends on

Used by

Dependency tree · two levels

16 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