Alphabeta MathHow 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 inner-product norm is definite, homogeneous, and satisfies the triangle inequality
Statement
The function induced by an inner product satisfies, for all vectors and scalars ,
Facts & Assumptions
Given: Vectors in a real or complex inner product space and a scalar .
The induced norm is a nonnegative square root, and positive definiteness detects the zero vector (The norm induced by a real or complex inner product).
The induced norm is homogeneous (Inner products separate vectors, and the induced norm is homogeneous: ).
Cauchy–Schwarz gives (Cauchy–Schwarz: , with equality exactly for linearly dependent vectors).
If , then and (Real and imaginary parts, complex conjugation, and modulus).
Proof
Nonnegativity and definiteness follow directly from [L1], and homogeneity is [L2].
Expanding and using conjugate symmetry gives . From [L4], , so ; now [L3] makes the expansion at most .
Both quantities in step 1.2 are nonnegative. If the left were larger, their squared order would also be larger, a contradiction. Hence the triangle inequality holds.
Depends on
- The norm $\lVert v\rVert=\sqrt{\langle v,v\rangle}$ induced by a real or complex inner product
- Inner products separate vectors, and the induced norm is homogeneous: $\lVert\lambda v\rVert=|\lambda|\lVert v\rVert$
- Cauchy–Schwarz: $|\langle u,v\rangle|\leq\lVert u\rVert\lVert v\rVert$, with equality exactly for linearly dependent vectors
- Real and imaginary parts, complex conjugation, and modulus
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 47 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Sheldon Axler, Linear Algebra Done Right, 4th ed., §6A (standard reference, not scraped)
- Sergei Treil, Linear Algebra Done Wrong, Ch. 5, §5.1 (standard reference, not scraped)