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 Euclidean inner product on
Definition
Let . A natural number is a von Neumann natural, that is a set, and (The natural numbers (von Neumann), On the order is membership: ), so
is the function space of The vector space of all functions with pointwise operations, and as the case at and , a vector space over under the pointwise operations (Vector space over a field). We write for , and two elements of are equal exactly when they agree at every . This is the same set that as the set of functions , and , , are metrics on it calls .
The Euclidean inner product of is the real number
the finite sum of Finite sums and finite products, by recursion applied to the list (extended by beyond , as every finite list in this library is). The Euclidean norm of is
which is defined because (a sum of nonnegative terms, Laws of finite sums and finite products clause 4 and Squares of nonzero elements are positive, the case giving by Integer powers ) and every nonnegative real has a unique nonnegative square root (Square roots exist: a unique with ; the positives are ).
Both are defined for every , including
At the set has exactly one element, the empty function, and it is the zero vector space (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension clause 5); the sum above is the empty sum, so and . This is the first place on this page where the two index regimes diverge, and the divergence is deliberate. The published metrics , , of as the set of functions , and , , are metrics on it are defined only for , because would otherwise be a maximum over the empty index set; the algebra above needs no such restriction. The boundary in this page runs between the algebra and the metric, not where a reader would guess, and Conventions of this page, the standing hypothesis, and what is taken up elsewhere in the reading order lists exactly which items inherit .
The algebra of the inner product
For all and :
- Symmetry. , since termwise.
- Additivity in the first argument. : the list is the termwise sum of and , so Laws of finite sums and finite products clause 1 applies.
- Homogeneity in the first argument. , by Laws of finite sums and finite products clause 2.
- Bilinearity. Clauses 2 and 3 together with symmetry give the same two laws in the second argument.
- Positive definiteness. , and if and only if . Indeed a vanishing sum of nonnegative terms has every term (Laws of finite sums and finite products clause 4), so for every , and a nonzero real has a positive square (Squares of nonzero elements are positive), whence for every and .
- Agreement with the published Euclidean metric. For and , , the two sides being the same expression ( as the set of functions , and , , are metrics on it). In particular .
That is a norm in the sense of A norm on a real vector space, the induced metric, and the dictionary with the metric axioms is proved in Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation, where the triangle inequality is obtained from the Cauchy-Schwarz inequality; it is not assumed here.
Definition references
The natural numbers (von Neumann)
The vector space of all functions with pointwise operations, and as the case
as the set of functions , and , , are metrics on it
Finite sums and finite products, by recursion
Laws of finite sums and finite products
Squares of nonzero elements are positive
Square roots exist: a unique with ; the positives are
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
Remarks
-
Scope: the concrete form only. What is defined above is the Euclidean inner product on and nothing more. The general theory of inner product spaces — abstract inner products, orthonormal bases, Gram-Schmidt, orthogonal projection and orthogonal complements of arbitrary subspaces — is developed elsewhere in this library. No item on this page claims anything about abstract inner product spaces, and no item on this page introduces the general notion.
-
The standard basis and coordinates. For the standard unit vector has and for (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ). Then : the list vanishes except at , where its value is , and a list vanishing off one index sums to its value there (Laws of finite sums and finite products clause 3, splitting the range at ). So the coordinates of are recovered by testing against the standard basis, which is the form used repeatedly below.
-
Powers here are integer powers. means the integer power of Integer powers , and by Square roots exist: a unique with ; the positives are and Laws of integer exponents.
Depends on
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
The vector space of all functions with pointwise operations, and as the case
Vector space over a field
The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension
Finite sums and finite products, by recursion
Laws of finite sums and finite products
as the set of functions , and , , are metrics on it
Squares of nonzero elements are positive
Square roots exist: a unique with ; the positives are
The natural numbers (von Neumann)
On the order is membership:
Integer powers
Laws of integer exponents