lean-matrix-cookbook
lean-matrix-cookbook copied to clipboard
eric-wieser
The matrix cookbook, proved in the Lean theorem prover
Clicking on the progress bar goes to URLs like https://github.com/eric-wieser/lean-matrix-cookbook/blob/1ef3514608dab634404e8cb0eb94160dc670f799/lib/MatrixCookbook/1Basic.lean#L72-L73 which is 404 and not the same as the new directory structure which doesn't have a `lib`. A few months...
Determinant and Trace are Product and Sum of Eigenvalues The eigenvalue as defined here is the same as the eigenvalue defined by `mathlib` for endomorphisms. 1. `root_charpoly_iff_has_eigenvalue` and lemmas for...
# Rank One Update by Concatenation of inverse Equation With $X$ an $(m+1)\times m$ matrix and $v$ a $(m+1)\times 1$ vector and $\alpha$ defined as: $$\alpha = v^Tv - v^TXAX^Tv$$...
Relatively straight forward rewrites to clearout the Searle Identities. - $(1 + A⁻¹)⁻¹ = A(A + 1)⁻¹$ - $(A + BBᵀ)⁻¹B = A⁻¹B(1 + BᵀA⁻¹B)⁻¹$ - $(A⁻¹ + B⁻¹)⁻¹ =...
# Exact Inverse Relations: Eq 146, 150, 156 through Eq 160 This Pull Request adds proofs for equations 156 through 160. In addition equations 156 and 158 have "Hermitianized" versions,...
# Main Changes ## DFT Matrix properties Equations 403 through 412 and definitions necessary to state these lemmas such as DFT/IDFT on vectors, the DFT and Inverse DFT matrices. We...
Metadata
Owner
Metadata
The matrix cookbook, proved in the Lean theorem prover