TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

Weighted AM-GM inequality with rational weights

Statement

Let $n \in N$ with $n \geq 1$ , let $x_{0}, \dots, x_{n - 1} \in R$ with $x_{k} > 0$ , and let $w_{0}, \dots, w_{n - 1} \in Q$ be rational weights with $w_{k} \geq 0$ (Order on the rationals) whose images under the canonical embedding $ι : Q \to R$ (The unique embedding of ℚ into an ordered field) satisfy $\sum_{k < n} ι (w_{k}) = 1$ . Then

$\prod_{k < n} x_{k}^{w_{k}} \leq \sum_{k < n} ι (w_{k}) x_{k},$

where $x_{k}^{w_{k}}$ is the rational power of Rational powers $a^{r}$ of a positive base.

Both sums are sums in $R$ , and that is not a detail. This library defines $\sum_{k < n}$ only for a sequence $N \to R$ (Finite sums and finite products, by recursion); there is no finite sum of rationals and none is used here. The weights are therefore summed after being carried into $R$ by $ι$ , and no step below sums anything outside $R$ . Nothing is lost by this reading, because $ι$ is an injective field homomorphism: for $n = 2$ the hypothesis $ι (w_{0}) + ι (w_{1}) = 1$ is exactly $w_{0} + w_{1} = 1$ in $Q$ , and the conclusion reads $x_{0}^{w_{0}} x_{1}^{w_{1}} \leq ι (w_{0}) x_{0} + ι (w_{1}) x_{1}$ . Below, $ι$ is kept visible wherever a rational is being used as a real; elsewhere the page follows the usual convention of writing $w$ for $ι (w)$ (Finite sums and finite products, by recursion).

Why the weights are rational. The restriction is not laziness and it cannot be relaxed here. For a real weight $w$ the symbol $x^{w}$ has no meaning in this library at all: Rational powers $a^{r}$ of a positive base defines $x^{r}$ only for $r \in Q$ , and every proof on this page is a finite chain of field operations together with the least-upper-bound property. Real exponents require the exponential function and its inverse, which are built much later and by different means; the closing remark of this page records the situation in full. Taking $n = 2$ and $w_{0} = w_{1} = 1 / 2$ recovers the two-term case $\sqrt{x_{0} x_{1}} \leq (x_{0} + x_{1}) / 2$ of The arithmetic mean, geometric mean inequality.

Facts & Assumptions

Given: A natural $n \geq 1$ , reals $x_{0}, \dots, x_{n - 1} > 0$ , and rationals $w_{0}, \dots, w_{n - 1} \geq 0$ with $\sum_{k < n} ι (w_{k}) = 1$ , a sum in $R$ .

[L1]

AM-GM (The arithmetic mean, geometric mean inequality): for $c_{0}, \dots, c_{N - 1} \geq 0$ with $N \geq 1$ , $(\prod_{i < N} c_{i})^{1 / N} \leq \frac{1}{N} \sum_{i < N} c_{i}$ .

[L2]

Finite sums and products, defined ONLY for sequences $N \to R$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products): the recursion clauses $\sum_{k < 0} a_{k} = 0$ and $\sum_{k < j + 1} a_{k} = \sum_{k < j} a_{k} + a_{j}$ ; splitting of sums and products at any index $m \leq m^{'}$ , $\sum_{k < m^{'}} a_{k} = \sum_{k < m} a_{k} + \sum_{k = m}^{m^{'} - 1} a_{k}$ , where the tail $\sum_{k = m}^{m^{'} - 1} a_{k}$ is by definition the shifted sum $\sum_{t < m^{'} - m} a_{m + t}$ (Finite sums and finite products, by recursion), and likewise for products; scaling $\sum_{k < m} λ a_{k} = λ \sum_{k < m} a_{k}$ ; and the constant sum $\sum_{i < m} λ = ι (m) λ$ . Every $\sum$ and $\prod$ written below is therefore a sum or product in $R$ .

[L3]

Constant product: $\prod_{i < m} λ = λ^{m}$ , by induction on $m$ from the recursion clauses $\prod_{i < m + 1} λ = (\prod_{i < m} λ) λ$ and $λ^{m + 1} = λ^{m} λ$ , with both sides equal to $1$ at $m = 0$ (Finite sums and finite products, by recursion, Integer powers $a^{m}$ , The principle of mathematical induction).

[L4]

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, v > 0$ and rationals $r, s$ : $u^{r} > 0$ , $(u v)^{r} = u^{r} v^{r}$ (hence, by induction on the number of factors, $(\prod_{j < n} u_{j})^{r} = \prod_{j < n} u_{j}^{r}$ , using also the constant product for the empty case), and $(u^{r})^{s} = u^{r s}$ .

[L5]

Rational arithmetic, the order on $Q$ and the embedding (Every rational has a positive-denominator representative, The rationals as equivalence classes of pairs of integers, Arithmetic on the rationals, Order on the rationals, The unique embedding of ℚ into an ordered field, Canonical naturals are positive and strictly increasing): on a representative with positive denominator, $m / N \geq 0$ holds exactly when $m \geq 0$ in $Z$ (Order on the rationals, with the order on $Z$ as in Order on the integers); a nonnegative integer is the image of a unique natural and a positive integer the image of a unique natural $\geq 1$ (The naturals embed in the integers), which is the step that licenses reading such an $m$ , and such a denominator, as a natural number; every single rational has a representative with positive denominator (Every rational has a positive-denominator representative states exactly this, for one rational; the passage to a common denominator for finitely many is NOT quoted from it and is carried out by the induction inside step 1.1); $ι : Q \to R$ is an injective order-preserving field homomorphism, so $ι (0) = 0$ , $ι (u + v) = ι (u) + ι (v)$ and $ι (u v) = ι (u) ι (v)$ ; on an integer $ι$ is $m \mapsto m \cdot 1_{R}$ , with $ι (m) > 0$ for a natural $m \geq 1$ and $m \mapsto ι (m)$ injective on ${1, 2, \dots}$ , hence injective on all of $N$ since $ι (0) = 0 < ι (m)$ there.

[L6]

Induction principle (The principle of mathematical induction), used for the routine inductions on the number of terms below, and the recursion theorem (The recursion theorem), which is what defines a function on $N$ by a recursion clause.

Proof

technique · direct

1.1

Common denominator, by an induction written out rather than asserted. The claim at $j$ is: any rationals $v_{0}, \dots, v_{j - 1}$ admit a natural $N \geq 1$ and integers $p_{0}, \dots, p_{j - 1}$ with $v_{k} = p_{k} / N$ for every $k < j$ . At $j = 0$ take $N = 1$ , there being no $p_{k}$ to produce. Assume the claim at $j$ and let $v_{0}, \dots, v_{j}$ be given: applying it to $v_{0}, \dots, v_{j - 1}$ yields a natural $N^{'} \geq 1$ and integers $p_{k}^{'}$ with $v_{k} = p_{k}^{'} / N^{'}$ , and $v_{j}$ has a representative $v_{j} = a / b$ with $b > 0$ , hence with $b$ a natural $\geq 1$ ; then $N : = N^{'} b$ is a natural $\geq 1$ , and the integers $p_{k} : = p_{k}^{'} b$ for $k < j$ and $p_{j} : = a N^{'}$ satisfy $p_{k} / N = (p_{k}^{'} b) / (N^{'} b) = p_{k}^{'} / N^{'} = v_{k}$ and $p_{j} / N = (a N^{'}) / (b N^{'}) = a / b = v_{j}$ , since $(x, y) \sim (x c, y c)$ for $c \neq 0$ . The claim at $j = n$ , applied to $w_{0}, \dots, w_{n - 1}$ , fixes a natural $N \geq 1$ and integers $m_{0}, \dots, m_{n - 1}$ with $w_{k} = m_{k} / N$ . Finally each $m_{k}$ is a natural: $w_{k} \geq 0$ read on the positive-denominator representative $m_{k} / N$ gives $m_{k} \geq 0$ in $Z$ , and a nonnegative integer is the image of a unique natural.

L5L6

2.1

The numerators sum to $ι (N)$ in $R$ : applying scaling to the real sequence $k \mapsto ι (w_{k})$ multiplies the hypothesis $\sum_{k < n} ι (w_{k}) = 1$ by $ι (N)$ to give $\sum_{k < n} ι (N) ι (w_{k}) = ι (N)$ , and $ι (N) ι (w_{k}) = ι (N w_{k}) = ι (m_{k})$ since $ι$ is multiplicative and $N w_{k} = m_{k}$ in $Q$ , so $\sum_{k < n} ι (m_{k}) = ι (N)$ .

step 1.1L2L5

2.2

The partial sums of the numerators, inside $N$ : define $M : N \to N$ by recursion, $M_{0} : = 0$ and $M_{j + 1} : = M_{j} + m_{j}$ for $j < n$ (and $M_{j + 1} : = M_{j}$ for $j \geq n$ ), so each $M_{j}$ is a natural number and $M_{j} \leq M_{j + 1}$ ; then $ι (M_{j}) = \sum_{k < j} ι (m_{k})$ for every $j \leq n$ , by induction on $j$ , since $ι (M_{0}) = ι (0) = 0 = \sum_{k < 0} ι (m_{k})$ and $ι (M_{j + 1}) = ι (M_{j}) + ι (m_{j}) = \sum_{k < j} ι (m_{k}) + ι (m_{j}) = \sum_{k < j + 1} ι (m_{k})$ by additivity of $ι$ and the recursion clause for finite sums.

step 1.1L2L5L6construct

3.1

Hence $M_{n} = N$ , an identity between natural numbers: steps 2.1 and 2.2 give $ι (M_{n}) = \sum_{k < n} ι (m_{k}) = ι (N)$ , and $m \mapsto ι (m)$ is injective on $N$ .

step 2.1step 2.2L5

4.1

The expanded list: define $c : N \to R$ by $c_{i} : = x_{j}$ whenever $M_{j} \leq i < M_{j + 1}$ for some $j < n$ , and $c_{i} : = 1$ for $i \geq N$ ; this covers every $i \in N$ exactly once, because the blocks $[M_{j}, M_{j + 1})$ for $j < n$ partition $[0, M_{n}) = [0, N)$ by step 3.1, and every $c_{i}$ with $i < N$ is positive since each $x_{j} > 0$ .

step 1.1step 2.2step 3.1L5construct

5.1

Its sum and product, by a second induction written out rather than asserted. The claim at $j \leq n$ is $\sum_{i < M_{j}} c_{i} = \sum_{k < j} ι (m_{k}) x_{k}$ and $\prod_{i < M_{j}} c_{i} = \prod_{k < j} x_{k}^{m_{k}}$ . At $j = 0$ we have $M_{0} = 0$ and all four expressions are the empty sum $0$ or the empty product $1$ . Assume the claim at $j < n$ . Since $M_{j} \leq M_{j + 1}$ , splitting gives $\sum_{i < M_{j + 1}} c_{i} = \sum_{i < M_{j}} c_{i} + \sum_{i = M_{j}}^{M_{j + 1} - 1} c_{i}$ , and the tail is by definition $\sum_{t < m_{j}} c_{M_{j} + t}$ , since $M_{j + 1} - M_{j} = m_{j}$ ; every one of its terms equals $x_{j}$ , because $M_{j} \leq M_{j} + t < M_{j + 1}$ for $t < m_{j}$ , so the constant sum evaluates it as $ι (m_{j}) x_{j}$ , and therefore $\sum_{i < M_{j + 1}} c_{i} = \sum_{k < j} ι (m_{k}) x_{k} + ι (m_{j}) x_{j} = \sum_{k < j + 1} ι (m_{k}) x_{k}$ by the recursion clause for finite sums. The same computation with products in place of sums, the constant product in place of the constant sum, gives $\prod_{i < M_{j + 1}} c_{i} = (\prod_{k < j} x_{k}^{m_{k}}) x_{j}^{m_{j}} = \prod_{k < j + 1} x_{k}^{m_{k}}$ . At $j = n$ , where $M_{n} = N$ by step 3.1, this reads $\sum_{i < N} c_{i} = \sum_{j < n} ι (m_{j}) x_{j}$ and $\prod_{i < N} c_{i} = \prod_{j < n} x_{j}^{m_{j}}$ .

step 3.1step 4.1L2L3L6

6.1

Applying AM-GM to $c_{0}, \dots, c_{N - 1}$ and substituting: $(\prod_{j < n} x_{j}^{m_{j}})^{1 / N} = (\prod_{i < N} c_{i})^{1 / N} \leq \frac{1}{N} \sum_{i < N} c_{i} = ι (N)^{- 1} \sum_{j < n} ι (m_{j}) x_{j} = \sum_{j < n} ι (w_{j}) x_{j}$ , the last equality by scaling together with $ι (N)^{- 1} ι (m_{j}) = ι (m_{j} / N) = ι (w_{j})$ .

step 4.1step 5.1L1L2L5

6.2

Rewriting the left-hand side with the rational power laws: $(\prod_{j < n} x_{j}^{m_{j}})^{1 / N} = \prod_{j < n} (x_{j}^{m_{j}})^{1 / N} = \prod_{j < n} x_{j}^{m_{j} / N} = \prod_{j < n} x_{j}^{w_{j}}$ , each $x_{j}^{m_{j}}$ being positive.

step 5.1L4L6

7.1

Combining the two displays gives $\prod_{j < n} x_{j}^{w_{j}} \leq \sum_{j < n} ι (w_{j}) x_{j}$ , which is the assertion.

step 6.1step 6.2∎

Depends on

Used by

Young's inequality for products (rational conjugate exponents) Theorem

Dependency tree · two levels

57 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

MIT 18.100A, AM-GM inequality handout (standard reference, not scraped)
Finite inequalities (Cornell University) (standard reference, not scraped)
AM-GM 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)