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.
Clarkson inequalities in both exponent ranges
Statement
Let be a measure space, let , and let over either or .
- If , then
- If and , then
At both formulas are the same equality.
Facts & Assumptions
Given: A measure space , a real number , and for or .
For , the conjugate exponent is and satisfies (Conjugate exponents, including the endpoint conventions).
Real powers on positive bases obey the product, quotient, and iterated power laws; is continuous and differentiable on with derivative (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, Continuity and derivatives of positive-base real powers).
The natural logarithm is the inverse of the exponential, is continuous and strictly increasing, obeys the product and quotient laws, and has derivative (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).
The sum, product, quotient, and chain rules compute derivatives; the sign of a derivative on an interval gives the corresponding monotonicity, and a continuous real function takes every intermediate value (Sums, scalar multiples, products and quotients: , , , and when , The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , On an interval , for continuous on and differentiable at every interior point: throughout gives nondecreasing, gives increasing, and give the two decreasing forms; conversely a nondecreasing has and a nonincreasing has wherever it is differentiable, and no strict converse is claimed, Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and ).
For conjugate finite exponents , two-term Hölder gives (Holder's inequality for finite sums and conjugate real exponents)
Real and complex consist of a.e. classes of measurable representatives with and addition, subtraction, scalar multiplication, and the norm are representative-independent (The function space for , Complex Lp classes and Euclidean test-function conventions, The norm descends to the quotient and makes a normed space for , Complex Holder, Minkowski, and the quotient norm).
The nonnegative integral is order preserving and positively homogeneous, and it is additive on two nonnegative measurable functions (Monotonicity and nonnegative homogeneity of the nonnegative integral, Additivity of the nonnegative Lebesgue integral).
Proof
Suppose and let . For , first : if , divide by and use for and ; the zero case is equality. Also . For this is equality. For , apply [F5] with conjugate and to and , then raise to the th power.
Suppose and put . For , define We will prove . Set and ; by [F1], . For , put and Direct differentiation gives G_1'(t)=\alpha t^{\alpha-2}H(t),\qquad H'(t)=2(\alpha+1)t(\beta-t^{\alpha-1})<0. \tag{2} because . The estimate holds whenever , while . Continuity, [F4], and strict decrease therefore give a unique at which vanishes. Thus increases before and decreases after it.
Suppose , put , , and . For measurable representatives of , let and . These numbers are finite by [F7]. If , the inequality below is immediate. If , set Then and . Two-term Hölder [F5], applied pointwise to and , gives M=\int_S(\lambda A+\eta B)\,d\mu\le\int_S(A^r+B^r)^{1/r}\,d\mu. \tag{7}
For real or complex scalars , [F6] and coordinate expansion give the scalar parallelogram identity Apply both inequalities of step 1.1, first to and then to . Since , this yields |a+b|^p+|a-b|^p\le2^{p-1}(|a|^p+|b|^p). \tag{1}
For every sufficiently small , for example the final inequality holds whenever . On the other hand , and strict decrease on gives there. Consequently continuity and the monotonicity from step 1.2 give a unique such that on and on .
Define, for , Using [F2]–[F4] and simplifying over the positive common denominator gives G_2'(t)=\frac{2G_1(t)}{(1-t^2)(1-t^{2\alpha})}. \tag{3} For every , implies ; hence as , and logarithm continuity proves that extends continuously by . By step 2.2 it first strictly decreases and then strictly increases. It eventually becomes positive: the derivative test applied to gives , while ; hence whenever . By the logarithm and real-power laws, the logarithm of the left side is , so it is positive there. Thus [F4] gives a unique such that on and on .
Choose measurable representatives of and ; every pointwise inequality below is unchanged by modifying them on a null set. If , integrate (1), use [F7]–[F8], and divide by : The integrals are finite because by the normed-space structure in [F7].
Put The two terms are positive. Since is strictly increasing, the sign of is the sign of the logarithm of their ratio, namely Another direct differentiation gives \Phi'(t)=\frac{\big((1+t)^q+(1-t)^q\big)^{1/q-1}}{(1+t^p)^{1+1/p}}G_3(t). \tag{4} The prefactor is positive. Step 3.1 therefore shows that decreases and then increases, so its maximum on is at an endpoint. Finally This proves \big((1+t)^q+(1-t)^q\big)^{1/q}\le2^{1/q}(1+t^p)^{1/p}. \tag{5}
For arbitrary real , the unordered pair equals . After swapping the two moduli and, when the larger one is nonzero, dividing by it, (5) gives (|a+b|^q+|a-b|^q)^{1/q}\le2^{1/q}(|a|^p+|b|^p)^{1/p}. \tag{6} The case is immediate.
The same estimate holds for complex . The case where either is zero follows directly, so swap them if necessary and suppose . Put , , and ; the last inequality follows from . The two terms below swap if changes sign, so For , let Its derivative is Thus . Apply (5) to , then multiply by using [F6], to obtain (6) over as well.
Raise the complex-or-real scalar estimate (6) to the th power. Since , it says pointwise that Use this in (7), then use [F7]–[F8]: Raising to gives a factor . Dividing by and using yields
Step 3.2 proves the first claim, and step 6.1 proves the second for . At one has , and the scalar parallelogram identity in step 2.1 integrates to equality, so the overlapping endpoint belongs to both claims and the two displayed formulas coincide. The empty measure space, zero measure, and zero functions cause no exception: all their norms and all terms above are zero.
Source notes
Kuriyama–Miyagi–Okada–Miyoshi prove the real one-variable maximum through their Lemmas 2.1–2.4 and Theorem 2.5, then pass to complex scalars and in Theorems 3.2 and 3.4. Steps 1.2, 2.2, 3.1, and 4.1 reproduce the derivative-sign argument rather than treating that strategy as proof text. Step 5.2 rewrites their phase calculation using , and step 1.3 spells out the two-coordinate Hölder duality behind the required integral inequality.
Depends on
- Conjugate exponents, including the endpoint conventions
- Real powers for positive bases, with the zero-base positive-exponent convention
- The natural logarithm as the inverse of the exponential function
- Real and imaginary parts, complex conjugation, and modulus
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
- Continuity and derivatives of positive-base real powers
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- On an interval $I$, for $f$ continuous on $I$ and differentiable at every interior point: $f' \ge 0$ throughout gives $f$ nondecreasing, $f' > 0$ gives $f$ increasing, $f' \le 0$ and $f' < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f' \ge 0$ and a nonincreasing $f$ has $f' \le 0$ wherever it is differentiable, and no strict converse is claimed
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- Holder's inequality for finite sums and conjugate real exponents
- The function space $\mathcal{L}^p(\mu)$ for $0 < p < \infty$
- Complex Lp classes and Euclidean test-function conventions
- The $L^p$ norm descends to the quotient and makes $L^p$ a normed space for $1 \le p \le \infty$
- Complex Holder, Minkowski, and the quotient norm
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- Additivity of the nonnegative Lebesgue integral
Used by
- Lᵖ is uniformly convex for 1<p<∞ Corollary
Dependency tree · two levels
102 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
- Kuriyama, Miyagi, Okada and Miyoshi, Elementary proof of Clarkson's inequalities and their generalization (standard reference, not scraped)