Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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.

Young's inequality for conjugate real exponents

Statement

Let p,q>1p,q>1 satisfy 1/p+1/q=11/p+1/q=1. For u,v≥0u,v\ge0, uv≤upp+vqq.uv\le\frac{u^p}{p}+\frac{v^q}{q}.

Facts & Assumptions

Given: Conjugate real exponents p,q>1p,q>1 and nonnegative reals u,vu,v.

[L1]

Weighted AM-GM applies to positive entries with nonnegative weights summing to one (The weighted arithmetic-geometric mean inequality for real weights).

[L2]

Positive-base real-power laws hold, and the zero-base convention is 0r=00^r=0 for r>0r>0; positive-base real powers are positive (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents, The exponential is positive and satisfies exp⁡(−x)=1/exp⁡(x)\exp(-x)=1/\exp(x)).

Proof

technique · direct
1.1

If u=0u=0 or v=0v=0, the inequality is immediate from nonnegativity of the two terms on the right.

L2
1.2

For u,v>0u,v>0, apply [L1] to up,vqu^p,v^q with weights 1/p,1/q1/p,1/q.

L1given
2.1

Its geometric side is (up)1/p(vq)1/q=uv(u^p)^{1/p}(v^q)^{1/q}=uv, and its arithmetic side is up/p+vq/qu^p/p+v^q/q.

step 1.2L2
3.1

Steps 1.1 and 2.1 cover all nonnegative u,vu,v.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources