Square root of a PSD linear map in Lean via Matrix.toLin on the eigenbasis
Mathlib's CFC sqrt does not apply to real inner product spaces (E →L[ℝ] E is not a C*-algebra). To get M with ‖M x‖² = ⟪Q x, x⟫ for symmetric PSD Q, take v := hQ.eigenvectorBasis rfl and μ := hQ.eigenvalues rfl, then set M := Matrix.toLin v.toBasis v.toBasis (Matrix.diagonal fun j => √(μ j)). LinearMap.det_toLin and Matrix.det_diagonal give det M = ∏ √μⱼ. Matrix.toLin_self takes both bases explicitly (toLin_self b b A j), and then sum_eq_single gives M (v j) = √μⱼ • v j. With open Finset, write Finset.prod_le_prod and Finset.prod_pow explicitly, because the bare names are ambiguous or resolve to the wrong lemma.
Mathlib v4.35.0 and v4.36.0-rc2:
Finset.prod_le_prodis now the ordered-monoid lemma ([MulLeftMono N] (h : ∀ i ∈ s, f i ≤ g i)), so writing the name out explicitly does not help over ℝ.Finset.prod_le_prod h0 hfails with 'Function expected', andFinset.prod_le_prod hfails onMulLeftMono ℝ. For nonnegative real factors like √μⱼ useFinset.prod_le_prod₀ h0 h, which compiles. The CFC point checks out:ContinuousFunctionalCalculus ℝ (E →L[ℝ] E) IsSelfAdjointandCStarAlgebra (E →L[ℝ] E)don't synthesize, whileCStarAlgebra (F →L[ℂ] F)does. eigenvectorBasis, eigenvalues, det_toLin, det_diagonal and toLin_self all exist as stated.