Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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 (S,A,μ) be a measure space, let 1<p<, and let f,gLp(μ) over either R or C.

  1. If p2, then f+g2pp+fg2ppfpp+gpp2.
  2. If 1<p2 and q=p/(p1), then f+g2pq+fg2pq(fpp+gpp2)q/p.

At p=2 both formulas are the same equality.

Facts & Assumptions

Given: A measure space (S,A,μ), a real number 1<p<, and f,gLp(μ;K) for K=R or C.

[F1]

For 1<p<, the conjugate exponent is q=p/(p1) and satisfies 1/p+1/q=1 (Conjugate exponents, including the endpoint conventions).

[F2]

Real powers on positive bases obey the product, quotient, and iterated power laws; xxa is continuous and differentiable on (0,) with derivative axa1 (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).

[F3]

The natural logarithm is the inverse of the exponential, is continuous and strictly increasing, obeys the product and quotient laws, and has derivative 1/x (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).

[F5]

For conjugate finite exponents r,s>1, two-term Hölder gives a1b1+a2b2(a1r+a2r)1/r(b1s+b2s)1/s. (Holder's inequality for finite sums and conjugate real exponents)

[F6]

For z=a+ib, one has z=(a2+b2)1/2, zw=zw, and z=0 exactly when z=0 (Real and imaginary parts, complex conjugation, and modulus, Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[F7]

Real and complex Lp consist of a.e. classes of measurable representatives with hpp=Shpdμ(1p<), and addition, subtraction, scalar multiplication, and the norm are representative-independent (The function space Lp(μ) for 0<p<, Complex Lp classes and Euclidean test-function conventions, The Lp norm descends to the quotient and makes Lp a normed space for 1p, Complex Holder, Minkowski, and the quotient norm).

[F8]

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

technique · prove the two scalar Clarkson estimates, then integrate; in the lower exponent range a two-coordinate Hölder calculation replaces an undeclared vector-valued Minkowski theorem
1.1

Suppose p2 and let r=p/21. For u,v0, first ur+vr(u+v)r: if u+v>0, divide by (u+v)r and use 0t1trt for t=u/(u+v) and 1t=v/(u+v); the zero case is equality. Also (u+v)r2r1(ur+vr). For r=1 this is equality. For r>1, apply [F5] with conjugate r and r/(r1) to (u,v) and (1,1), then raise to the rth power.

F2F4F5
1.2

Suppose 1<p<2 and put q=p/(p1)>2. For 0t1, define Φ(t)=((1+t)q+(1t)q)1/q(1+tp)1/p. We will prove Φ(t)21/q. Set α=p1 and β=1/(q1); by [F1], 0<α=β<1. For 0<t<1, put G1(t)=1t2ααβtα1+αβtα+1 and H(t)=(α+1)βt22tα+1+(1α)β. 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 tα1>1>β. The estimate H(t)>0 holds whenever 2tα+1<(1α)β, while H(1)=2(β1)<0. Continuity, [F4], and strict decrease therefore give a unique t0(0,1) at which H vanishes. Thus G1 increases before t0 and decreases after it.

F1F2F4
1.3

Suppose 1<p<2, put q=p/(p1), r=q/p>1, and s=r/(r1). For measurable representatives of f,g, let A=f+gp,B=fgp,U=SAdμ,V=SBdμ, and M=(Ur+Vr)1/r. These numbers are finite by [F7]. If M=0, the inequality below is immediate. If M>0, set λ=(U/M)r1,η=(V/M)r1. Then λs+ηs=1 and M=λU+ηV. Two-term Hölder [F5], applied pointwise to (λ,η) and (A,B), gives M=\int_S(\lambda A+\eta B)\,d\mu\le\int_S(A^r+B^r)^{1/r}\,d\mu. \tag{7}

F1F2F5F7F8
2.1

For real or complex scalars a,b, [F6] and coordinate expansion give the scalar parallelogram identity a+b2+ab2=2(a2+b2). Apply both inequalities of step 1.1, first to u=a+b2,v=ab2 and then to u=a2,v=b2. Since 2r=p, this yields |a+b|^p+|a-b|^p\le2^{p-1}(|a|^p+|b|^p). \tag{1}

step 1.1F2F6
2.2

For every sufficiently small t>0, G1(t)1+αβαβtα1<0; for example the final inequality holds whenever t1α<αβ/(1+αβ). On the other hand G1(1)=0, and strict decrease on (t0,1) gives G1(t)>0 there. Consequently continuity and the monotonicity from step 1.2 give a unique t1(0,t0) such that G1<0 on (0,t1) and G1>0 on (t1,1).

step 1.2F2F4
3.1

Define, for 0<t<1, G2(t)=log(1+t)+βlog(1tα)log(1t)βlog(1+tα). 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 ε>0, 0<t<ε1/α implies 0<tα<ε; hence tα0 as t0, and logarithm continuity proves that G2 extends continuously by G2(0)=0. By step 2.2 it first strictly decreases and then strictly increases. It eventually becomes positive: the derivative test applied to 1tαα(1t) gives 1tαα(1t), while 1+tα2; hence 1+t1t(1tα1+tα)β(α2)β(1t)β1>1 whenever 0<1t<(α/2)β/(1β). By the logarithm and real-power laws, the logarithm of the left side is G2(t), so it is positive there. Thus [F4] gives a unique t2(t1,1) such that G2<0 on (0,t2) and G2>0 on (t2,1).

step 2.2F2F3F4
3.2

Choose measurable representatives of f and g; every pointwise inequality below is unchanged by modifying them on a null set. If p2, integrate (1), use [F7]–[F8], and divide by 2p: f+g2pp+fg2ppfpp+gpp2. The integrals are finite because f±gLp by the normed-space structure in [F7].

step 2.1F7F8
4.1

Put G3(t)=(1+t)q1(1tp1)(1t)q1(1+tp1). The two terms are positive. Since log is strictly increasing, the sign of G3 is the sign of the logarithm of their ratio, namely (q1)log(1+t)+log(1tp1)(q1)log(1t)log(1+tp1)=(q1)G2(t). 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 [0,1] is at an endpoint. Finally Φ(0)=21/q,Φ(1)=221/p=211/p=21/q. This proves \big((1+t)^q+(1-t)^q\big)^{1/q}\le2^{1/q}(1+t^p)^{1/p}. \tag{5}

step 3.1F1F2F3F4
5.1

For arbitrary real a,b, the unordered pair {a+b,ab} equals {a+b,ab}. 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 a=b=0 is immediate.

step 4.1F2
5.2

The same estimate holds for complex a,b. The case where either is zero follows directly, so swap them if necessary and suppose ab>0. Put w=b/a, r=w1, and x=Rewr; the last inequality follows from r2=(Rew)2+(Imw)2. The two terms below swap if Rew changes sign, so 1+wq+1wq=(1+r2+2x)q/2+(1+r22x)q/2. For 0c1, let K(c)=(1+r2+2rc)q/2+(1+r22rc)q/2. Its derivative is K(c)=qr((1+r2+2rc)q/21(1+r22rc)q/21)0. Thus K(x/r)K(1)=(1+r)q+(1r)q. Apply (5) to r, then multiply by a using [F6], to obtain (6) over C as well.

step 4.1F2F4F6
6.1

Raise the complex-or-real scalar estimate (6) to the pth power. Since pr=q, it says pointwise that (Ar+Br)1/r2p/q(fp+gp). Use this in (7), then use [F7]–[F8]: (f+gpq+fgpq)p/q2p/q(fpp+gpp). Raising to q/p gives a factor 2. Dividing by 2q and using 1q=q/p yields f+g2pq+fg2pq(fpp+gpp2)q/p.

step 1.3step 5.1step 5.2F1F2F7F8
7.1

Step 3.2 proves the first claim, and step 6.1 proves the second for 1<p<2. At p=2 one has q=2, 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.

step 2.1step 3.2step 6.1F1F7F8

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 Lp 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 Rew/w, and step 1.3 spells out the two-coordinate Hölder duality behind the required integral inequality.

Depends on

Used by

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