TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

Hölder's inequality for finite sums (rational exponents)

Statement

Let $n \in N$ , let $a_{0}, \dots, a_{n - 1}$ and $b_{0}, \dots, b_{n - 1}$ be reals, and let $p, q \in Q$ with $p, q > 1$ and $\frac{1}{p} + \frac{1}{q} = 1$ be conjugate exponents (Young's inequality for products (rational conjugate exponents)). Then

$\sum_{k < n} ∣ a_{k} b_{k} ∣ \leq (\sum_{k < n} ∣ a_{k} ∣^{p})^{1 / p} (\sum_{k < n} ∣ b_{k} ∣^{q})^{1 / q} .$

All powers here are rational powers of nonnegative bases (Rational powers $a^{r}$ of a positive base): the exponents $p, q, 1 / p, 1 / q$ are positive rationals, so the supplementary clause $0^{r} = 0$ covers the vanishing bases and no expression is left undefined. Taking $p = q = 2$ gives $\sum_{k < n} ∣ a_{k} b_{k} ∣ \leq (\sum_{k < n} a_{k}^{2})^{1 / 2} (\sum_{k < n} b_{k}^{2})^{1 / 2}$ , since $x^{1 / 2} = \sqrt{x}$ and $∣ a_{k} ∣^{2} = a_{k}^{2}$ . That is not literally the root form of The Cauchy-Schwarz inequality for finite sums, whose left-hand side is $∣ \sum_{k < n} a_{k} b_{k} ∣$ : the two are bridged by $∣ \sum_{k < n} c_{k} ∣ \leq \sum_{k < n} ∣ c_{k} ∣$ (Triangle inequality for finite sums), which is the only step needed to get from the display above to the root form.

Facts & Assumptions

Given: A natural $n$ , reals $a_{0}, \dots, a_{n - 1}$ and $b_{0}, \dots, b_{n - 1}$ , and conjugate rationals $p, q > 1$ . Write $S : = \sum_{k < n} ∣ a_{k} ∣^{p}$ , $T : = \sum_{k < n} ∣ b_{k} ∣^{q}$ , $P : = S^{1 / p}$ and $Q : = T^{1 / q}$ .

[L1]

Young's inequality (Young's inequality for products (rational conjugate exponents)): $u v \leq \frac{u^{p}}{p} + \frac{v^{q}}{q}$ for all reals $u, v \geq 0$ .

[L2]

Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): additivity, scaling, monotonicity, and the fact that a sum of nonnegative terms is nonnegative and vanishes only if every term vanishes.

[L3]

Rational power laws (Laws of rational exponents, Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): for $u > 0$ and rationals $r, s$ : $u^{r} > 0$ , $(u^{r})^{s} = u^{r s}$ , $u^{1} = u$ , $u^{- r} = (u^{r})^{- 1}$ , and $(u v)^{r} = u^{r} v^{r}$ , the last also for $u, v \geq 0$ when $r > 0$ ; and $0^{r} = 0$ for rational $r > 0$ , while $u > 0$ gives $u^{r} > 0$ .

[L4]

Absolute values (Basic properties of the absolute value, Absolute value in an ordered field): $∣ x ∣ \geq 0$ , $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ , and $∣ x ∣ = 0$ only for $x = 0$ .

[L5]

Order arithmetic: adding inequalities, that is $u \leq v$ and $u^{'} \leq v^{'}$ imply $u + u^{'} \leq v + v^{'}$ , and scaling a $\leq$ by a positive element. Order is preserved by adding a constant and by adding inequalities and Sign rules for products and monotonicity of multiplication state both moves for the STRICT order and only that, so the nonstrict forms used below are those statements together with the case of equality, which trichotomy settles (Ordered field); and inverses of positives are positive (Inverses of positives are positive, and reciprocation reverses order, claim 1). The rational coefficients $1 / p$ and $1 / q$ are read as elements of $R$ through the unique injective order-preserving field embedding of $Q$ (The unique embedding of ℚ into an ordered field, Order on the rationals); the rational exponents $p$ and $q$ remain elements of $Q$ and act through Rational powers $a^{r}$ of a positive base.

Proof

technique · direct

1.1

All the quantities are defined and nonnegative: each $∣ a_{k} ∣^{p} \geq 0$ and each $∣ b_{k} ∣^{q} \geq 0$ , so $S \geq 0$ and $T \geq 0$ , and since $1 / p > 0$ and $1 / q > 0$ the powers $P = S^{1 / p}$ and $Q = T^{1 / q}$ are defined and nonnegative.

L2L3L4

2.1

Degenerate cases: if $S = 0$ then every $∣ a_{k} ∣^{p} = 0$ , so every $∣ a_{k} ∣ = 0$ (a positive base has positive powers) and hence every $a_{k} = 0$ , making the left-hand side $\sum_{k < n} ∣ a_{k} b_{k} ∣ = 0$ , while $P = 0^{1 / p} = 0$ makes the right-hand side $0$ as well; the case $T = 0$ is symmetric, so the inequality holds and we may assume $S > 0$ and $T > 0$ , hence $P > 0$ and $Q > 0$ .

step 1.1L2L3L4

3.1

Normalisation identities: $P^{p} = (S^{1 / p})^{p} = S^{(1 / p) p} = S^{1} = S$ , and likewise $Q^{q} = T$ ; moreover for each $k$ , $(∣ a_{k} ∣ P^{- 1})^{p} = ∣ a_{k} ∣^{p} (P^{- 1})^{p} = ∣ a_{k} ∣^{p} (P^{p})^{- 1} = ∣ a_{k} ∣^{p} S^{- 1}$ , and likewise $(∣ b_{k} ∣ Q^{- 1})^{q} = ∣ b_{k} ∣^{q} T^{- 1}$ .

step 2.1L3

4.1

Termwise Young, applied to $u = ∣ a_{k} ∣ P^{- 1} \geq 0$ and $v = ∣ b_{k} ∣ Q^{- 1} \geq 0$ : for every $k < n$ , $∣ a_{k} ∣ ∣ b_{k} ∣ P^{- 1} Q^{- 1} \leq \frac{1}{p} ∣ a_{k} ∣^{p} S^{- 1} + \frac{1}{q} ∣ b_{k} ∣^{q} T^{- 1}$ .

step 3.1L1L3L5

5.1

Summing over $k < n$ and using additivity and scaling: $P^{- 1} Q^{- 1} \sum_{k < n} ∣ a_{k} ∣ ∣ b_{k} ∣ \leq \frac{1}{p} S^{- 1} \sum_{k < n} ∣ a_{k} ∣^{p} + \frac{1}{q} T^{- 1} \sum_{k < n} ∣ b_{k} ∣^{q} = \frac{1}{p} + \frac{1}{q} = 1$ , the middle equality because $S^{- 1} S = 1$ and $T^{- 1} T = 1$ .

step 4.1step 2.1L2L5

6.1

Multiplying by $P Q > 0$ and using $∣ a_{k} b_{k} ∣ = ∣ a_{k} ∣ ∣ b_{k} ∣$ gives $\sum_{k < n} ∣ a_{k} b_{k} ∣ \leq P Q$ , which together with the degenerate cases is the assertion.

step 5.1step 2.1L4L5∎

Depends on

Used by

Minkowski's inequality for finite sums (rational exponent) Theorem

Dependency tree · two levels

46 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. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
Finite inequalities (Cornell University) (standard reference, not scraped)
Young, Hölder, and Minkowski inequalities (Oregon State University) (standard reference, not scraped)
Hölder's inequality (Wikipedia) (standard reference, not scraped)
Young's inequality for products (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)