Thin singular value decomposition

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

/-!
# dm2017 def:thin-svd

Notation convention (dm2017 book.md:105, opening the section `# Linear Algebra`,
which contains the subsection `## The Singular Value Decomposition.` where this
definition appears). The section presents "basic linear algebraic facts and
notation" and assumes "basic familiarity with linear algebra (e.g., inner/outer
products of vectors, basic matrix operations such as addition, scalar
multiplication, transposition, ..., matrix multiplication, ...)".

This file reads the target's undefined notation with that standard meaning:
* `Xᵀ` / `X^T` is `Matrix.transpose`;
* juxtaposed matrix products such as `U Σ Vᵀ` and `UᵀU` are Mathlib matrix
  multiplication `*`;
* `I` is the identity matrix `1`;
* the outer product `u_i v_iᵀ` is `Matrix.vecMulVec`;
* `σ_i u_i v_iᵀ` is scalar multiplication `•`, and `∑` is the finite matrix sum.

The convention adds no hypothesis beyond what the target states locally.
-/

namespace RNLAPhaseB.DM2017ThinSVD

/-- The singular values of `A` (with multiplicity): the square roots of the
eigenvalues of the symmetric positive semidefinite matrix `Aᴴ * A` (`= Aᵀ * A`
over ℝ). This is a multiset, so no ordering convention of Mathlib's eigenvalue
enumeration is used. -/
noncomputable def singularValueMultiset {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
    Multiset ℝ :=
  (Finset.univ : Finset (Fin n)).val.map
    (fun j => Real.sqrt ((Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues j))

/-- The non-zero singular values of `A`, with multiplicity. -/
noncomputable def nonzeroSingularValueMultiset {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) : Multiset ℝ := by
  classical
  exact (singularValueMultiset A).filter (fun x => x ≠ 0)

/-- dm2017 def:thin-svd. For `A ∈ ℝ^{m×n}` of rank `ρ`, a thin SVD is
`A = U Σ Vᵀ = ∑_{i=1}^ρ σ_i u_i v_iᵀ`. Here `U ∈ ℝ^{m×ρ}` and `V ∈ ℝ^{n×ρ}` have
orthonormal columns (`UᵀU = I`, `VᵀV = I`) containing the left and right singular
vectors of `A` for the non-zero singular values. `Σ ∈ ℝ^{ρ×ρ}` is diagonal, with
the non-zero singular values of `A` in decreasing order on the diagonal.

Transposition, matrix products, the identity and outer products are read with
their standard meanings, per the Linear Algebra section's notation convention
(dm2017 book.md:105): `ᵀ` is `Matrix.transpose`, products are `*`, `I` is `1`,
and `u_i v_iᵀ` is `Matrix.vecMulVec`. -/
structure IsThinSVD {m n ρ : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (U : Matrix (Fin m) (Fin ρ) ℝ) (S : Matrix (Fin ρ) (Fin ρ) ℝ)
    (V : Matrix (Fin n) (Fin ρ) ℝ) : Prop where
  /-- `ρ` is the rank of `A`. -/
  rank_eq : A.rank = ρ
  /-- `A = U Σ Vᵀ`. -/
  factorization : A = U * S * Vᵀ
  /-- `A = ∑_{i=1}^ρ σ_i u_i v_iᵀ`. -/
  outer_sum : A = ∑ i : Fin ρ, S i i • Matrix.vecMulVec (fun r => U r i) (fun c => V c i)
  /-- `UᵀU = I`. -/
  U_orthonormal : Uᵀ * U = 1
  /-- `VᵀV = I`. -/
  V_orthonormal : Vᵀ * V = 1
  /-- The columns of `V` are right singular vectors: `A v_i = σ_i u_i`. -/
  right_singular_vectors : A * V = U * S
  /-- The columns of `U` are left singular vectors: `Aᵀ u_i = σ_i v_i`. -/
  left_singular_vectors : Aᵀ * U = V * S
  /-- `Σ` is diagonal. -/
  S_diag : S.IsDiag
  /-- The diagonal of `Σ` consists exactly of the non-zero singular values of `A`
  (with multiplicity). -/
  S_diag_eq_nonzero_singular_values :
    (Finset.univ : Finset (Fin ρ)).val.map (fun i => S i i) = nonzeroSingularValueMultiset A
  /-- The diagonal entries appear in decreasing (non-increasing) order. -/
  S_antitone : Antitone (fun i : Fin ρ => S i i)

/-- The source's stated range of the rank: `ρ ≤ min{m,n}`. -/
theorem rank_le_min {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
    A.rank ≤ min m n := by sorry

end RNLAPhaseB.DM2017ThinSVD