TheoremStatement: AI-adaptedProof: AI-adaptedprecheck pass

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), written with the same symbols $w_{k}$ in field arithmetic, 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 field equality $w_{0} + w_{1} = 1$ is equivalent by injectivity to the same equality in $Q$ , and the conclusion reads $x_{0}^{w_{0}} x_{1}^{w_{1}} \leq w_{0} x_{0} + w_{1} x_{1}$ . Throughout the statement and proof, a rational used as a field coefficient or a summand denotes its image under the bare inclusion $ι$ (Finite sums and finite products, by recursion); a rational used as an exponent retains its original rational type. Natural list lengths and index bounds also retain their natural type.

Why the weights are rational. This theorem uses the rational powers of Rational powers $a^{r}$ of a positive base, which are the powers available at this point in the reading order. Arbitrary real weights are outside this theorem's scope; real powers for positive bases are defined later through the exponential and logarithm in the later definition of real powers. That later construction is the library's chosen development, rather than a logical necessity for defining real powers or proving their laws, as the closing remark of this page explains. 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 and therefore preserves zero, addition, products and inverses. Rational symbols in real sums and scalar products below denote their images through this map. On an integer the embedding is $m \mapsto m \cdot 1_{R}$ ; its image is positive for natural $m \geq 1$ , and this map is injective on all of $N$ , including zero. Injectivity is used to pass from equality of field images to equality of natural numerator sums.

[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.1L5L6

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.

2.1step 1.1L2L5

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} = m_{k}$ in the field by multiplicativity of the embedding applied to the rational identity $N w_{k} = m_{k}$ , so $\sum_{k < n} m_{k} = N$ .

2.2step 1.1L2L5L6construct

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 natural and $M_{j} \leq M_{j + 1}$ . Its canonical field image is $M_{j} \cdot 1_{R} = \sum_{k < j} m_{k}$ for $j \leq n$ , the sum being real under the convention in [L5]. Indeed the identity holds at zero; additivity of the embedding gives $(M_{j} + m_{j}) \cdot 1_{R} = M_{j} \cdot 1_{R} + m_{j} \cdot 1_{R}$ , and the real finite-sum recursion then gives the successor identity.

3.1step 2.1step 2.2L5

Hence $M_{n} = N$ as natural numbers: steps 2.1 and 2.2 give $M_{n} \cdot 1_{R} = \sum_{k < n} m_{k} = N \cdot 1_{R}$ , and the map $m \mapsto m \cdot 1_{R}$ is injective on $N$ . This licenses the natural list length N in the next step; it is not an identification of arbitrary reals with indices.

4.1step 1.1step 2.2step 3.1L5construct

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

5.1step 3.1step 4.1L2L3L6

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

6.1step 4.1step 5.1L1L2L5

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

6.2step 5.1L4L6

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.

7.1step 6.1step 6.2∎

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

Weighted AM-GM inequality with rational weights

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources