feat(Analysis/InnerProductSpace/Adjoint): characterize least-squares minimizers#42122

bocowgill wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

bocowgill:ols-linear-mapbocowgill/mathlib4:ols-linear-mapCopy head branch name to clipboard