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 Cauchy-Schwarz inequality for finite sums

Statement

Let $n \in N$ and let $a_{0}, \dots, a_{n - 1}$ and $b_{0}, \dots, b_{n - 1}$ be reals, with finite sums as in Finite sums and finite products, by recursion. Then

$(\sum_{k < n} a_{k} b_{k})^{2} \leq (\sum_{k < n} a_{k}^{2}) (\sum_{k < n} b_{k}^{2}),$

and, in root form (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ),

$∣ \sum_{k < n} a_{k} b_{k} ∣ \leq \sqrt{\sum_{k < n} a_{k}^{2}} \sqrt{\sum_{k < n} b_{k}^{2}} .$

Equality holds in the first display if and only if the two lists are proportional, in the symmetric sense that there is a pair $(λ, μ) \neq (0, 0)$ of reals with $λ a_{k} = μ b_{k}$ for every $k < n$ .

No root is used in the proof of the squared form. That form is an identity plus a sign argument in the ordered field, and the root form is only a restatement of it through the monotonicity of squaring on the nonnegatives (Squaring is monotone on the nonnegatives); the root enters nowhere but the last step, where that restatement is made and Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ is what supplies the square-root symbol. This matters here, because it makes the squared inequality independent of the existence theorem for roots.

Facts & Assumptions

Given: A natural $n$ and reals $a_{0}, \dots, a_{n - 1}$ , $b_{0}, \dots, b_{n - 1}$ . Write $A : = \sum_{k < n} a_{k}^{2}$ , $B : = \sum_{k < n} a_{k} b_{k}$ and $C : = \sum_{k < n} b_{k}^{2}$ .

[L1]

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.

[L2]

Squares (Squares of nonzero elements are positive, Integer powers $a^{m}$ ): $x^{2} \geq 0$ for every $x$ , and $x^{2} = 0$ only for $x = 0$ ; and a product with a zero factor vanishes, $0 \cdot x = 0$ (Multiplication by zero: $0 \cdot a = 0$ ).

[L3]

Square roots (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ): every $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ .

[L4]

Monotonicity of squaring (Squaring is monotone on the nonnegatives): for $x, y \geq 0$ , $x \leq y ⟺ x^{2} \leq y^{2}$ ; and $∣ x ∣^{2} = x^{2}$ with $∣ x ∣ \geq 0$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L5]

Order arithmetic in an ordered field: adding inequalities (Order is preserved by adding a constant and by adding inequalities) and scaling an inequality by a positive element (Sign rules for products and monotonicity of multiplication, claim 4) are both stated there for the STRICT order alone, so the nonstrict uses below are those statements together with the case of equality, settled by trichotomy (Ordered field); the inverse of a positive element is positive (Inverses of positives are positive, and reciprocation reverses order, claim 1); and a nonzero factor cancels, since $λ x = 0$ with $λ \neq 0$ gives $x = λ^{- 1} (λ x) = λ^{- 1} \cdot 0 = 0$ , a product with a zero factor (Multiplication by zero: $0 \cdot a = 0$ ).

Proof

technique · direct

1.1

For every $t \in R$ each term $(a_{k} t + b_{k})^{2}$ is nonnegative, so the sum is nonnegative, and expanding with additivity and scaling gives $0 \leq \sum_{k < n} (a_{k} t + b_{k})^{2} = A t^{2} + 2 B t + C$ .

L1L2

1.2

In particular $A \geq 0$ and $C \geq 0$ , being sums of squares.

L1L2

1.3

Proportionality forces equality: assume $λ a_{k} = μ b_{k}$ for all $k < n$ with $(λ, μ) \neq (0, 0)$ ; if $μ \neq 0$ then $b_{k} = c a_{k}$ with $c = λ / μ$ , so $B = c A$ and $C = c^{2} A$ by scaling, whence $B^{2} = c^{2} A^{2} = A (c^{2} A) = A C$ ; and if $μ = 0$ then $λ \neq 0$ forces $a_{k} = 0$ for all $k$ , so $A = B = 0$ and both sides vanish.

L1L5

2.1

Suppose first $A = 0$ : then every term of $\sum_{k < n} a_{k}^{2}$ vanishes, so $a_{k} = 0$ for all $k < n$ , hence $B = \sum_{k < n} 0 \cdot b_{k} = 0$ and both sides of the squared inequality are $0$ , so it holds with equality; and the pair $(λ, μ) = (1, 0)$ satisfies $λ a_{k} = 0 = μ b_{k}$ .

step 1.2L1L2

2.2

Suppose instead $A > 0$ and substitute $t = - B / A$ into step 1.1: $0 \leq A \frac{B^{2}}{A^{2}} - 2 \frac{B^{2}}{A} + C = C - \frac{B^{2}}{A}$ , so $\frac{B^{2}}{A} \leq C$ , and multiplying by $A > 0$ gives $B^{2} \leq A C$ .

step 1.1step 1.2L5

3.1

The squared inequality therefore holds in both cases, which exhaust the possibilities since $A \geq 0$ .

step 2.1step 2.2step 1.2

3.2

Equality forces proportionality: in the case $A = 0$ this was step 2.1; in the case $A > 0$ , if $B^{2} = A C$ then putting $t_{0} = - B / A$ in step 1.1 gives $\sum_{k < n} (a_{k} t_{0} + b_{k})^{2} = A t_{0}^{2} + 2 B t_{0} + C = C - \frac{B^{2}}{A} = 0$ , so every term vanishes and $b_{k} = - t_{0} a_{k}$ for all $k$ , and the pair $(λ, μ) = (- t_{0}, 1) \neq (0, 0)$ works.

step 1.1step 2.1step 2.2L1L2L5

4.1

The root form: by step 3.1, $∣ B ∣^{2} = B^{2} \leq A C = (\sqrt{A} \sqrt{C})^{2}$ , and both $∣ B ∣$ and $\sqrt{A} \sqrt{C}$ are nonnegative, so monotonicity of squaring on the nonnegatives gives $∣ B ∣ \leq \sqrt{A} \sqrt{C}$ ; note also that $\sqrt{A} \sqrt{C}$ is the nonnegative square root of $A C$ , by uniqueness.

step 3.1step 1.2L3L4∎

Depends on

Used by

Dependency tree · two levels

30 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)
Young, Hölder, and Minkowski inequalities (Oregon State University) (standard reference, not scraped)
Cauchy-Schwarz inequality (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (Thm 1.35) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §7.1 (standard reference, not scraped)