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.

The arithmetic mean, geometric mean inequality

Statement

Let $n \in N$ with $n \geq 1$ and let $a_{0}, \dots, a_{n - 1} \in R$ with $a_{k} \geq 0$ for every $k < n$ . Write

$A : = \frac{1}{n} \sum_{k < n} a_{k}, G : = (\prod_{k < n} a_{k})^{1 / n},$

the arithmetic mean and the geometric mean, where the $n$ -th root exists because $\prod_{k < n} a_{k} \geq 0$ (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Laws of finite sums and finite products) and $n$ denotes the canonical natural $ι (n) \in R$ , which is invertible since $n \geq 1$ (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field). Then

$\prod_{k < n} a_{k} \leq A^{n}, equivalently G \leq A,$

and equality holds in either form if and only if $a_{0} = a_{1} = \dots = a_{n - 1}$ .

The proof is Cauchy's forward-backward induction: the statement is proved first along a doubling sequence, by doubling, and then pulled back from a member of that sequence to every smaller $n$ by a descent that replaces the missing entry with the arithmetic mean of the others. That is why the induction below runs over the doubling scheme and not over $n$ directly.

One point of hygiene decides how the doubling scheme is written. The doubling index has to be a natural number, because it is used as the length of a list, as a bound on an index, and as the starting point of a descent. The symbol $2^{j}$ would not do: Integer powers $a^{m}$ defines powers of a real base, so $2^{j}$ denotes the real number $ι (2)^{j}$ , which is not a natural number and cannot index anything. The doubling sequence is therefore defined inside $N$ , by recursion (The recursion theorem):

$N_{0} = 1, N_{j + 1} = N_{j} + N_{j} (j \in N),$

and the induction below runs over $j$ , with $N_{j}$ as the list length. No identity relating $N_{j}$ to any real power is needed anywhere, and none is claimed.

Facts & Assumptions

Given: A natural $n \geq 1$ and reals $a_{0}, \dots, a_{n - 1} \geq 0$ ; for $m \geq 1$ let $P (m)$ denote the statement "for all reals $b_{0}, \dots, b_{m - 1} \geq 0$ , $\prod_{k < m} b_{k} \leq B^{m}$ where $B = \frac{1}{m} \sum_{k < m} b_{k}$ , with equality if and only if $b_{0} = \dots = b_{m - 1}$ ".

[L1]

A product with a zero factor is zero, $0 \cdot x = 0$ (Multiplication by zero: $0 \cdot a = 0$ ). Laws of finite sums and products (Laws of finite sums and finite products, Finite sums and finite products, by recursion): splitting of sums and of products at any index; the constant sum $\sum_{k < m} λ = m λ$ ; monotonicity of sums, with a sum of nonnegatives being $0$ only if every term is $0$ ; and a product of nonnegatives is nonnegative, of positives positive.

[L2]

Roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): every $c \geq 0$ has a unique $c^{1 / m} \geq 0$ with $(c^{1 / m})^{m} = c$ , and $c^{1 / m} > 0$ when $c > 0$ .

[L3]

Power monotonicity (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Integer powers $a^{m}$ ): $x \mapsto x^{m}$ is strictly increasing and injective on ${x \geq 0}$ for $m \geq 1$ , and preserves nonnegativity and positivity.

[L4]

Integer exponent laws (Laws of integer exponents): $(x y)^{m} = x^{m} y^{m}$ and $(x^{2})^{m} = x^{2 m}$ .

[L5]

Order arithmetic: multiplying inequalities of nonnegatives, in both the strict and the nonstrict form (Multiplying inequalities of positives); adding inequalities and scaling by a positive, both of which Order is preserved by adding a constant and by adding inequalities and Sign rules for products and monotonicity of multiplication state for the STRICT order only, so the nonstrict forms used below are the strict ones together with the case of equality, which is settled by trichotomy (Ordered field); and the inverse of a positive element is positive (Inverses of positives are positive, and reciprocation reverses order).

[L6]

Squares: $x^{2} \geq 0$ , which is $x^{2} > 0$ for $x \neq 0$ (Squares of nonzero elements are positive, the only thing that item states) together with $0^{2} = 0 \cdot 0 = 0$ , a product with a zero factor (Multiplication by zero: $0 \cdot a = 0$ ); and $x^{2} = 0$ only for $x = 0$ , the contrapositive of the same statement.

[L7]

Induction principle (The principle of mathematical induction).

[L8]

The doubling naturals: by the recursion theorem (The recursion theorem) applied to the set $N$ , the starting element $1$ and the function $f (k) = k + k$ , there is a unique $j \mapsto N_{j}$ from $N$ to $N$ with $N_{0} = 1$ and $N_{j + 1} = N_{j} + N_{j}$ . Each $N_{j}$ is a natural number, available as a list length and as an index bound; the real number $ι (2)^{j}$ is never used and never mentioned.

[L9]

Canonical naturals: $ι (m) > 0$ for $m \geq 1$ , $ι$ is a field homomorphism, and we write $m$ for $ι (m)$ (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field).

[L10]

Order and addition in $N$ (Order on the natural numbers, $\leq$ is a linear order on $N$ , Order is compatible with addition, Discreteness: $σ (n)$ is the immediate successor, Addition is associative, Addition is commutative): $\leq$ is a linear order; $m \leq n$ holds exactly when $n = m + i$ for some $i \in N$ ; $m \leq n$ holds exactly when $m + k \leq n + k$ and $m < n$ exactly when $m + k < n + k$ , BOTH forms being stated in Order is compatible with addition and the nonstrict one being the one step 1.5 uses; $m < n$ holds exactly when $m + 1 \leq n$ (Discreteness: $σ (n)$ is the immediate successor); and addition is associative and commutative.

Proof

technique · induction

1.1

Base case $P (1)$ : for a single entry $b_{0} \geq 0$ we have $\prod_{k < 1} b_{k} = b_{0}$ and $B = \frac{1}{1} b_{0} = b_{0}$ , so $\prod_{k < 1} b_{k} = b_{0} = B^{1}$ ; equality always holds, and the condition "all entries equal" is automatic for one entry.

baseL1L9

1.2

Inductive hypothesis: fix $j \in N$ , write $N : = N_{j}$ for the $j$ -th doubling natural, and assume $P (N)$ .

1.3

Reduction to positive entries: if some $b_{k} = 0$ then $\prod_{k < m} b_{k} = 0 \leq B^{m}$ , and equality means $B^{m} = 0$ , hence $B = 0$ , hence $\sum_{k < m} b_{k} = 0$ , hence every $b_{k} = 0$ , that is, all entries equal; conversely all entries equal to $0$ gives both sides $0$ ; so $P (m)$ holds for lists with a zero entry, and it is enough to prove $P (m)$ for lists of strictly positive entries.

L1L2L3L9

1.4

The two-entry case $P (2)$ : for $x, y \geq 0$ , $(\frac{x + y}{2})^{2} - x y = \frac{(x + y)^{2} - 4 x y}{4} = (\frac{x - y}{2})^{2} \geq 0$ , so $x y \leq (\frac{x + y}{2})^{2}$ , with equality exactly when $(\frac{x - y}{2})^{2} = 0$ , that is when $x = y$ .

L5L6L9

1.5

The doubling naturals grow past their index: $N_{j} \geq 1$ and $N_{j} > j$ for every $j \in N$ , by induction on $j$ inside $N$ ; at $j = 0$ , $N_{0} = 1 \geq 1$ and $1 > 0$ ; and if $N_{j} \geq 1$ and $N_{j} > j$ , then $N_{j} \geq j + 1$ , so $N_{j + 1} = N_{j} + N_{j} \geq (j + 1) + 1 > j + 1$ and $N_{j + 1} \geq 1 + 1 \geq 1$ . This inequality is between natural numbers throughout; nothing is transported into $R$ .

L7L8L10

2.1

Doubling step, $P (N) \Rightarrow P (2 N)$ , where $2 N : = N + N = N_{j + 1}$ is again a natural number: let $a_{0}, \dots, a_{2 N - 1} > 0$ , put $X : = \frac{1}{N} \sum_{k < N} a_{k}$ and $Y : = \frac{1}{N} \sum_{k = N}^{2 N - 1} a_{k}$ , both positive, and let $A : = \frac{1}{2 N} \sum_{k < 2 N} a_{k}$ ; splitting the sum at $N$ gives $\sum_{k < 2 N} a_{k} = N X + N Y$ , so $A = \frac{X + Y}{2}$ ; splitting the product at $N$ and applying the hypothesis to each half gives $\prod_{k < 2 N} a_{k} = (\prod_{k < N} a_{k}) (\prod_{k = N}^{2 N - 1} a_{k}) \leq X^{N} Y^{N} = (X Y)^{N}$ ; and the two-entry case applied to $X, Y$ gives $X Y \leq (\frac{X + Y}{2})^{2} = A^{2}$ , whence $(X Y)^{N} \leq (A^{2})^{N} = A^{2 N}$ and therefore $\prod_{k < 2 N} a_{k} \leq A^{2 N}$ .

step 1.2step 1.3step 1.4L1L3L4L5L9

2.2

Descent step, $P (m + 1) \Rightarrow P (m)$ for every natural $m \geq 1$ , written in this direction so that no subtraction of naturals is needed: let $b_{0}, \dots, b_{m - 1} > 0$ and put $B : = \frac{1}{m} \sum_{k < m} b_{k} > 0$ ; define $a_{k} : = b_{k}$ for $k < m$ and $a_{m} : = B$ , so that $\sum_{k < m + 1} a_{k} = m B + B = (m + 1) B$ and the arithmetic mean of $a_{0}, \dots, a_{m}$ is exactly $B$ ; applying $P (m + 1)$ gives $(\prod_{k < m} b_{k}) B = \prod_{k < m + 1} a_{k} \leq B^{m + 1}$ , and dividing by $B > 0$ gives $\prod_{k < m} b_{k} \leq B^{m}$ ; moreover equality here holds exactly when $\prod_{k < m + 1} a_{k} = B^{m + 1}$ , which by the equality clause of $P (m + 1)$ holds exactly when all of $a_{0}, \dots, a_{m}$ are equal, that is when $b_{0} = \dots = b_{m - 1} = B$ , which in turn holds exactly when the $b_{k}$ are all equal, since a constant list equals its own mean; together with the zero-entry case this is $P (m)$ .

step 1.3L1L3L5L9

3.1

Equality in the doubling step: with the notation of the doubling step 2.1, suppose $\prod_{k < 2 N} a_{k} = A^{2 N}$ ; then both inequalities in the chain are equalities, so first $(X Y)^{N} = (A^{2})^{N}$ with $X Y, A^{2} > 0$ gives $X Y = A^{2}$ by injectivity, hence $X = Y$ by the equality clause of the two-entry case; and second, writing $P_{1} = \prod_{k < N} a_{k} \leq X^{N}$ and $P_{2} = \prod_{k = N}^{2 N - 1} a_{k} \leq Y^{N}$ with all four quantities positive, $P_{1} < X^{N}$ would give $P_{1} P_{2} < X^{N} P_{2} \leq X^{N} Y^{N}$ , so $P_{1} = X^{N}$ and likewise $P_{2} = Y^{N}$ , whence by the equality clause of $P (N)$ the first half is constant, equal to its mean $X$ , and the second half is constant, equal to $Y = X$ ; so all $2 N$ entries are equal, and conversely entries all equal to $c$ give $\prod = c^{2 N}$ and $A = c$ .

step 1.2step 1.4step 2.1L1L3L5L9

4.1

By the induction principle, $P (N_{j})$ holds for every $j \in N$ : the base is $P (N_{0}) = P (1)$ and the step is the doubling argument together with its equality clause.

step 1.1step 2.1step 3.1L7L8

5.1

Every $n \geq 1$ is reached: by step 1.5, $N_{n} > n$ , so $n \leq N_{n}$ and $N_{n} = n + i_{0}$ for some $i_{0} \in N$ ; now run a further induction on $i$ over the statement $Q (i)$ , "for every natural $m \geq 1$ with $m + i = N_{n}$ , $P (m)$ holds"; $Q (0)$ says $P (N_{n})$ , which is step 4.1; and if $Q (i)$ holds and $m \geq 1$ satisfies $m + (i + 1) = N_{n}$ , then $(m + 1) + i = N_{n}$ with $m + 1 \geq 1$ , so $P (m + 1)$ holds by $Q (i)$ and the descent step turns it into $P (m)$ , giving $Q (i + 1)$ ; applying $Q (i_{0})$ to $m = n$ yields $P (n)$ ; hence $\prod_{k < n} a_{k} \leq A^{n}$ with equality exactly when all $a_{k}$ are equal.

step 1.5step 4.1step 2.2L7L10

6.1

Translation to the root form: $G = (\prod_{k < n} a_{k})^{1 / n}$ satisfies $G \geq 0$ and $G^{n} = \prod_{k < n} a_{k} \leq A^{n}$ with $A \geq 0$ , so $G \leq A$ , since $G > A$ would give $G^{n} > A^{n}$ ; and $G = A$ holds exactly when $G^{n} = A^{n}$ , by injectivity of $x \mapsto x^{n}$ on the nonnegatives, hence exactly when all $a_{k}$ are equal.

step 5.1L2L3discharge-induction∎

Depends on

Used by

∏_j ≥ 0 (1 + (-1)ʲ/√j+2) has partial products tending to 0 although ∑_j ≥ 0 (-1)ʲ/√j+2 converges Counterexample
The Cauchy product of ∑_k ≥ 0 (-1)ᵏ/√k+1 with itself has |cₙ| ≥ 1 for every n, so it diverges Counterexample
FALSE: the Cauchy product of two convergent series converges False statement
n^1/n → 1 Lemma
Weighted AM-GM inequality with rational weights Theorem

Dependency tree · two levels

52 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)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)