Alphabeta MathHow 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 satisfy . For ,
Facts & Assumptions
Given: Conjugate real exponents and nonnegative reals .
Weighted AM-GM applies to positive entries with nonnegative weights summing to one (The weighted arithmetic-geometric mean inequality for real weights).
Positive-base real-power laws hold, and the zero-base convention is for ; 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 ).
Proof
If or , the inequality is immediate from nonnegativity of the two terms on the right.
For , apply [L1] to with weights .
Its geometric side is , and its arithmetic side is .
Steps 1.1 and 2.1 cover all nonnegative .
Depends on
- The weighted arithmetic-geometric mean inequality for real weights
- 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)$
Used by
- Graded MINI mass initialization can destroy the smooth instantaneous pressure rate Counterexample
- Absorption of lower-order Sobolev terms in the elliptic estimate Lemma
- Caccioppoli inequality for truncated subsolutions Lemma
- Ehrling-type Hölder and derivative interpolation with an epsilon loss Lemma
- Freezing coefficients makes the Schauder error absorbable on a small ball Lemma
- Logarithmic Caccioppoli estimate for positive supersolutions Lemma
- Tangential H² estimate near a flat Dirichlet boundary Lemma
- The difference-quotient test function and its commutators Lemma
- Backward Euler MINI step existence and discrete energy bound Theorem
- Compact Laplace-type bundle operators: regularity and shifted parametrices Theorem
- De Giorgi local boundedness of homogeneous subsolutions Theorem
- Equality in Holder's inequality for 1 < p < ∞ Theorem
- Exterior-sphere elliptic Dirichlet existence, energy and residual stability Theorem
- Garding's inequality for a divergence-form elliptic operator Theorem
- Global H² Dirichlet regularity Theorem
- Holder's inequality for finite sums and conjugate real exponents Theorem
- Holder's inequality for integrals, including the endpoint cases Theorem
- Interior H² estimate for constant-coefficient elliptic equations Theorem
- Interior H² regularity for divergence-form equations Theorem
- Nonlinear backward Euler Galerkin existence and energy bounds Theorem
- Quantitative residual error under strong monotonicity Theorem
- Smooth-branch velocity error for backward Euler MINI Theorem
- The Caccioppoli inequality for weak elliptic solutions Theorem
Dependency tree · two levels
11 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
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)