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.
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation
Statement
Let and let , with the Euclidean inner product and the Euclidean norm as in The Euclidean inner product on . Then:
- Cauchy-Schwarz. with equality if and only if there is a pair of reals with for every .
- is a norm on (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), for every ; the metric it induces is of as the set of functions , and , , are metrics on it whenever .
- Parallelogram law.
- Polarisation. so the inner product is recovered from the norm it induces.
Clause 1 is a citation, not a new proof. The inequality and its equality case are the published The Cauchy-Schwarz inequality for finite sums, stated there for two lists of reals; all that happens below is that it is read in the vector notation of The Euclidean inner product on . Re-proving it here would put two proofs of one statement in the library.
Statement references
Facts & Assumptions
Given: A natural number and vectors , so that and (The Euclidean inner product on , Finite sums and finite products, by recursion).
Cauchy-Schwarz for finite sums (The Cauchy-Schwarz inequality for finite sums): , with equality if and only if there is with for every ; and the root form .
The inner product is symmetric, bilinear and positive definite, , and exactly when (The Euclidean inner product on , Laws of finite sums and finite products).
Square roots (Square roots exist: a unique with ; the positives are ): every has a unique with , written ; hence and (Integer powers ).
Squaring is monotone on the nonnegatives: for , if and only if , and if and only if (Squaring is monotone on the nonnegatives).
Absolute value (Basic properties of the absolute value, Absolute value in an ordered field): , , and .
The norm axioms (N1), (N2), (N3) (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), and the fact that for ( as the set of functions , and , , are metrics on it, The Euclidean inner product on clause 6).
Proof
Instantiating [L1] at and gives , with equality exactly when some has for every .
Both and are nonnegative, and their squares are and .
Expanding by bilinearity and symmetry, .
The same expansion at gives .
For a scalar , , so .
Axiom (N1) holds: if and only if , which by positive definiteness says .
Comparing the squares of step 1.2 through step 1.1 and using monotonicity of squaring on the nonnegatives yields , with equality exactly in the proportional case of step 1.1; this is clause 1.
Adding the identities of step 1.3 and step 1.4 gives , which is clause 3.
Subtracting the identity of step 1.4 from that of step 1.3 gives , which is clause 4 after dividing by .
Both and are nonnegative and by step 1.5 have equal squares, so , which is axiom (N2).
By step 2.1 the middle term of step 1.3 satisfies , so .
Both and are nonnegative, so step 3.1 and monotonicity of squaring give , which is axiom (N3).
Steps 2.4, 1.6 and 4.1 are exactly (N1), (N2) and (N3), so is a norm on for every , and for the metric it induces is ; this is clause 2, and with steps 2.1, 2.2 and 2.3 all four clauses are proved.
Remarks
-
Which route to the triangle inequality was taken. The proof above obtains (N3) by expanding and applying Cauchy-Schwarz. The alternative is to quote Minkowski's inequality for finite sums (rational exponent) at the rational exponent , which states the same inequality directly; that route is equally legitimate and is the one Each is a norm on , and the induced metrics are exactly , and of the published metric-spaces page uses for a general exponent. Only one of the two is used here, so no statement is proved twice.
-
Clause 1 holds at , where it reads , and the equality case is then satisfied by every pair , the condition quantifying over no indices. Clause 2 also holds at , the zero space carrying exactly one norm (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). What is not available at is the metric of as the set of functions , and , , are metrics on it, which is why the last sentence of clause 2 carries .
-
Clauses 3 and 4 are what the companion page uses. The parallelogram law is an identity satisfied by every norm of the form , so a norm violating it is not of that form; that is how the companion page rules out on . Polarisation says the inner product carries no information the norm does not.
Depends on
The Euclidean inner product on
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
The Cauchy-Schwarz inequality for finite sums
Minkowski's inequality for finite sums (rational exponent)
Laws of finite sums and finite products
Finite sums and finite products, by recursion
Square roots exist: a unique with ; the positives are
Squaring is monotone on the nonnegatives
as the set of functions , and , , are metrics on it
Integer powers
Basic properties of the absolute value
Absolute value in an ordered field