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.

Minkowski's inequality for integrals, including p=∞

Statement

Let (X,A,μ) be a measure space.

  1. If 1≤p<∞ and f,g∈Lp(μ), then ∥f+g∥p≤∥f∥p+∥g∥p.
  2. If f,g∈L∞(μ), then ∥f+g∥∞≤∥f∥∞+∥g∥∞.

Facts & Assumptions

Given: A measure space and functions f,g in the spaces named in the relevant clause of the Statement.

[L1]

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

[L3]

If h∈L∞(μ), then ∣h∣≤∥h∥∞ almost everywhere (The essential supremum is attained as the least essential bound).

[L4]

The nonnegative integral is monotone and homogeneous (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[L5]

The nonnegative integral is additive (Additivity of the nonnegative Lebesgue integral).

[L6]

Holder's inequality for finite sums gives, for nonnegative reals a,b, a+b≤21/q(ap+bp)1/p when q=p/(p−1) (Holder's inequality for finite sums and conjugate real exponents).

Proof

technique · For $1 < p < infinity$, first use the two-term finite Holder inequality to show $|f + g|^p$ is integrable, then apply the standard Holder step to $|f + g| |f + g|^{p - 1}$. The cases $p = 1$ and $p = \infty$ are handled directly from subadditivity of absolute value and the essential-supremum bound
1.1L4L5given

If p=1, then ∣f+g∣≤∣f∣+∣g∣ pointwise, so [L4, L5, given] ∥f+g∥1=∫∣f+g∣ dμ≤∫∣f∣ dμ+∫∣g∣ dμ=∥f∥1+∥g∥1.

1.2L1L2L4L5L6givenalgebra

Assume 1<p<∞ and let q:=p/(p−1). Then [L1, L2, L4, L5, L6, given, algebra] ∫∣f+g∣p dμ≤2p−1(∫∣f∣p dμ+∫∣g∣p dμ)<∞. Indeed, [L6] applied pointwise to the two-term families (∣f(x)∣,∣g(x)∣) and (1,1) gives ∣f(x)∣+∣g(x)∣≤21/q(∣f(x)∣p+∣g(x)∣p)1/p, so ∣f+g∣p≤(∣f∣+∣g∣)p≤2p−1(∣f∣p+∣g∣p) pointwise. Thus f+g∈Lp(μ). Put C:=∥f+g∥p. If C=0, the claim is immediate. Otherwise ∣f+g∣p=∣f+g∣ ∣f+g∣p−1≤∣f∣ ∣f+g∣p−1+∣g∣ ∣f+g∣p−1. Because (p−1)q=p, the function ∣f+g∣p−1 lies in Lq(μ) and has q-norm Cp−1. Integrating and applying [L1] with conjugate exponents p and q to each term yields Cp≤∥f∥p(∫∣f+g∣(p−1)q dμ)1/q+∥g∥p(∫∣f+g∣(p−1)q dμ)1/q. Since (p−1)q=p, this becomes Cp≤(∥f∥p+∥g∥p)Cp−1. If C>0, divide by Cp−1 to obtain the claim.

1.3L2L3given

For p=∞, let M:=∥f∥∞ and N:=∥g∥∞. Then [L2, L3, given] ∣f+g∣≤∣f∣+∣g∣≤M+N. Indeed, outside the union of the two null exceptional sets supplied by [L3], one has ∣f∣≤M and ∣g∣≤N. Therefore ∥f+g∥∞≤M+N.

2.1step 1.1step 1.2step 1.3∎

Steps 1.1, 1.2, and 1.3 prove the p=1, 1<p<∞, and p=∞ cases.

Depends on

Used by

Dependency tree · two levels

29 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