LeanDLR: a machine-checked Lean 4 + Mathlib library for dynamical low-rank approximation (DLRA): projector calculus, robust KSL/BUG error bounds, stability, conservation, low-rank training. No sorry, standard axioms only.
Lean Updated 6 days ago 1 commits
prism-dev|Mirror: thomascamminady/leandlr (⭐0)
6 days agoAbout
LeanDLR: a machine-checked Lean 4 + Mathlib library for dynamical low-rank approximation (DLRA): projector calculus, robust KSL/BUG error bounds, stability, conservation, low-rank training. No sorry, standard axioms only.
Readme