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.1L2L3L4

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.

2.1step 1.1L2L3L4

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$ .

3.1step 2.1L3

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}$ .

4.1step 3.1L1L3L5

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}$ .

5.1step 4.1step 2.1L2L5

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$ .

6.1step 5.1step 2.1L4L5∎

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.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources