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 standard formulas on and on are inner products
Statement
For and , the formulas
define inner products, linear in the first argument. At , the unique pairing on the zero space is an inner product.
Facts & Assumptions
Given: A natural number and the two displayed coordinate pairings.
Finite products in a commutative monoid have an empty value and may be read additively as finite sums (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity).
Complex conjugation preserves sums and products, and , with equality exactly when (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
The standard unit vectors form an ordered basis of , including (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ).
An inner product is linear in the first argument, conjugate symmetric, positive on the diagonal, and definite (Real and complex inner product spaces, with the inner product linear in the first argument).
Proof
Distributivity of the finite sums in [L1] gives linearity in the first variable. In the complex case [L2] gives conjugate-linearity in the second and conjugate symmetry; in the real case conjugation is the identity.
On the diagonal, the real formula is and the complex formula is . Each is nonnegative and vanishes only when every coordinate is zero, which by [L3] means the vector is zero.
Hence all the axioms in [L4] hold. When , the sum is empty and equals , while the zero vector is the only vector, so definiteness is valid.
Depends on
- Real and complex inner product spaces, with the inner product linear in the first argument
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
Used by
- A worked QR factorisation of an invertible real matrix Example
- Bessel's inequality is strict for a vector outside the span of a proper orthonormal set Example
- Gram–Schmidt on an explicit basis of ℂ² with conjugation visible Example
- Gram–Schmidt on an explicit basis of ℝ³ Example
- Projection onto a plane in ℝ³ and the nearest-point calculation Example
- The adjoint of an explicit map ℂ²→ℂ³ is its conjugate-transpose matrix Example
- The Riesz representative of an explicit functional on ℂ³ Example
- FALSE: Every complex inner product satisfies ⟨ u,v⟩=⟨ v,u⟩ False statement
- FALSE: Every orthogonal set is an orthonormal basis False statement
- FALSE: On a complex inner product space, (λ T)^*=λ T^* for every scalar False statement
- On ℝⁿ, abstract Cauchy–Schwarz is exactly the published finite-sum Cauchy–Schwarz inequality Proposition
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 78 results over 22 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, Example 6.3 (standard reference, not scraped)