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 Frobenius inner product on a real or complex matrix space
Example
On , where or , the formula
defines the Frobenius inner product, and
Facts & Assumptions
Given: Matrices of one fixed shape.
Matrices of a fixed shape form a vector space under entrywise operations (The vector space of by matrices over a field, with entrywise operations).
An inner product must be linear in its first argument, conjugate symmetric, positive, and definite (Real and complex inner product spaces, with the inner product linear in the first argument).
Complex conjugation distributes over finite sums and satisfies , vanishing exactly at (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Empty finite sums have additive value zero (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity).
Verification
Entrywise operations and finite-sum algebra give linearity in . Applying conjugation termwise and using [L3] gives conjugate symmetry.
On the diagonal, [L3] gives the displayed sum of squared moduli. It is nonnegative and vanishes exactly when every entry vanishes, which by [L1] means . Hence [L2] is satisfied.
If or , the matrix space contains only its zero matrix and [L4] makes the formula zero, so definiteness remains valid.
Depends on
- Real and complex inner product spaces, with the inner product linear in the first argument
- The vector space $M_{m \times n}(F) := F^{\,m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations
- 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
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
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: 56 results over 14 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
- Sergei Treil, Linear Algebra Done Wrong, Example 5.1.3 (standard reference, not scraped)