Commit 2026-03-23 22:20 15edd7a4

View on Github →

feat(Analysis/InnerProductSpace): definition of singular values for finite-dimensional inner product spaces (#33731) This PR defines the singular values for linear maps between finite-dimensional inner product spaces. The API is designed in a way that allows it to be generalized to the approximation numbers, as defined in #32126. See the discussion on Zulip: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Singular.20Value.20Decomposition/with/558914024

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/SingularValues.lean

added theorem LinearMap.card_support_singularValues

added theorem LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValues

added theorem LinearMap.injective_iff_forall_lt_finrank_singularValues_pos

added theorem LinearMap.isLowerSet_support_singularValues

added theorem LinearMap.singularValues_antitone

added theorem LinearMap.singularValues_eq_zero_iff

added theorem LinearMap.singularValues_eq_zero_iff_le_finrank_range

added theorem LinearMap.singularValues_fin

added theorem LinearMap.singularValues_finrank_range_self

added theorem LinearMap.singularValues_nonneg

added theorem LinearMap.singularValues_of_finrank_le

added theorem LinearMap.singularValues_of_lt

added theorem LinearMap.singularValues_pos_iff_lt_finrank_range

added theorem LinearMap.singularValues_pos_iff_ne_zero

added theorem LinearMap.singularValues_zero

added theorem LinearMap.sq_singularValues_fin

added theorem LinearMap.sq_singularValues_of_lt

added theorem LinearMap.support_singularValues