feat(Mathlib/Analysis): Existence of Singular Value Decomposition

[CodeTitanium]

This PR develops the Singular Value Decomposition (SVD) for complex matrices Matrix (Fin m) (Fin n) ℂ. It starts from the thin SVD for positive definite Gram matrices and extends to full rectangular SVD for arbitrary rectangular shapes.

Summary:

• Works over ℂ-valued matrices with Fin indices.
• Uses the existing spectral theorem for Hermitian matrices to obtain singular values and singular vectors.
• States unitary hypotheses using Matrix.unitaryGroup instead of ad‑hoc equalities.
• Describes diagonal factors via Matrix.diagonal for square pieces and a rectDiagonal constructor for rectangular factors.

Main results:

• IsRealDiag - Predicate for square complex matrices with real diagonal entries and zeros off-diagonal, together with basic API showing these matrices are Hermitian and self‑adjoint.
• exists_thinSVD_of_posDef
• Rectangular SVD
• The proof uses Gram–Schmidt (gramSchmidtOrthonormalBasis) to extend the nonzero left singular vectors to a full orthonormal basis.
• exists_rectSVD_wide (wide case, m ≤ n)

Proofs are organized around existing mathlib APIs (IsHermitian, PosDef, PosSemidef, spectral theorem, Gram–Schmidt).

---

[github-actions]

PR summary 6025bca1ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsRealDiag
+ IsRealDiag.diag_off
+ IsRealDiag.isHermitian_conjTranspose_eq
+ SigmaOf
+ SigmaOf_apply
+ SigmaPinvOf
+ SigmaPinvOf_apply
+ SigmaPinv_conjTranspose
+ SigmaPinv_isRealDiag
+ SigmaPinv_mul_Sigma_diag
+ Sigma_mul_SigmaPinv_diag
+ UhU_diag_core
+ exists_pseudoSVD_factorization
+ exists_rectSVD
+ exists_rectSVD_wide
+ exists_thinSVD_of_posDef
+ rectDiagonal

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[CodeTitanium]

I am changing the location of the code from Mathlib/LinearAlgebra to either Mathlib/Analysis or Mathlib/Topology due to errors of the form like this:
warning: Mathlib/LinearAlgebra/CheckForSVD.lean:22:0: Modules starting with Mathlib.LinearAlgebra are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic