Documentation

LeanMlir.Proofs.Foundation.Muon.SpectralForm

Spectral-form algebra for the Muon files #

The two moves MuonGeometry (shampoo_eq_muon) and MuonNewtonSchulz (nsStep_spectral) both make on a matrix written as A (diagonal p) Bᵀ: transposing it swaps the outer factors (svdForm_transpose), and a product of two such forms whose inner factors contract (BᵀC = 1) multiplies the diagonals pointwise (svdForm_mul).

source
theorem Proofs.MuonSpectral.svdForm_transpose {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) (p : Fin n → ℝ) :
(A * Matrix.diagonal p * B.transpose).transpose = B * Matrix.diagonal p * A.transpose

Transposing a spectral form swaps its outer factors: (A Σ Bᵀ)ᵀ = B Σ Aᵀ.

source
theorem Proofs.MuonSpectral.svdForm_mul {n : ℕ} (A B C D : Matrix (Fin n) (Fin n) ℝ) (p q : Fin n → ℝ) (h : B.transpose * C = 1) :
A * Matrix.diagonal p * B.transpose * (C * Matrix.diagonal q * D.transpose) = (A * Matrix.diagonal fun (i : Fin n) => p i * q i) * D.transpose

Two spectral forms multiply pointwise when the inner factors contract: BᵀC = 1 ⟹ (A (diag p) Bᵀ)(C (diag q) Dᵀ) = A (diag p·q) Dᵀ.