inductive Matrix.HasAbsolutelyPermutationSymmetricSingularValueFactorization {m n : ℕ} (g : Matrix (Fin m) (Fin n) ℝ → EReal) : Prop

An absolutely permutation symmetric singular-value factorization of g consists of an associated function on ℝ^(min m n) whose composition with singular_value_function recovers g.

• mk {m n : ℕ} {g : Matrix (Fin m) (Fin n) ℝ → EReal} (associatedFunction : (Fin (min m n) → ℝ) → EReal) (associatedFunction_isAbsolutelyPermutationSymmetric : Function.IsAbsolutelyPermutationSymmetric associatedFunction) (comp_eq : g = associatedFunction ∘ singular_value_function) : HasAbsolutelyPermutationSymmetricSingularValueFactorization g

theorem Matrix.rectangularDiagonal_conjTranspose_mul_eq_squared_tail {m n : ℕ} (x : Fin (min m n) → ℝ) : (rectangularDiagonal x).conjTranspose * rectangularDiagonal x = diagonal fun (j : Fin n) => if h : ↑j < min m n then x ⟨↑j, h⟩ ^ 2 else 0

Helper for Definition 7.19: the Gram matrix of a rectangular diagonal matrix is the diagonal matrix whose first min m n entries are the squared diagonal values and whose remaining entries are zero.

theorem Matrix.squared_tail_antitone {m n : ℕ} (x : Fin (min m n) → ℝ) (hx_nonneg : ∀ (i : Fin (min m n)), 0 ≤ x i) (hx_antitone : Antitone x) : Antitone fun (j : Fin n) => if h : ↑j < min m n then x ⟨↑j, h⟩ ^ 2 else 0

Helper for Definition 7.19: squaring a nonnegative antitone diagonal profile and appending zeros preserves antitonicity.

theorem Matrix.diagonal_eigenvalues_zero_indexed_eq {n : ℕ} (y : Fin n → ℝ) (hy : Antitone y) : let A := diagonal y; have hA := ⋯; hA.eigenvalues₀ = fun (j : Fin (Fintype.card (Fin n))) => y (Fin.cast ⋯ j)

Helper for Definition 7.19: a real diagonal matrix with antitone diagonal entries has ordered eigenvalue list equal to that diagonal.

theorem Matrix.singular_value_function_rectangularDiagonal_eq_of_nonneg_antitone {m n : ℕ} (x : Fin (min m n) → ℝ) (hx_nonneg : ∀ (i : Fin (min m n)), 0 ≤ x i) (hx_antitone : Antitone x) : singular_value_function (rectangularDiagonal x) = x

Helper for Definition 7.19: a rectangular diagonal matrix with a nonnegative antitone diagonal profile has that profile as its ordered singular-value vector.

theorem Matrix.exists_matrix_with_singular_value_function_eq_abs_descendingRearrangement {m n : ℕ} (x : Fin (min m n) → ℝ) : ∃ (X : Matrix (Fin m) (Fin n) ℝ), singular_value_function X = Function.descendingRearrangement fun (i : Fin (min m n)) => |x i|

Helper for Definition 7.19: every vector in ℝ^(min m n) can be realized as the ordered singular-value vector of some matrix after passing to the decreasing rearrangement of its absolute coordinates.

theorem Matrix.matrix_const_zero_symmetric_factorization {m n : ℕ} : (fun (x : Matrix (Fin m) (Fin n) ℝ) => 0) = (fun (x : Fin (min m n) → ℝ) => 0) ∘ singular_value_function

Helper for Definition 7.19: the constant zero singular-value profile factors the constant zero matrix-valued function through singular_value_function.

theorem Matrix.HasAbsolutelyPermutationSymmetricSingularValueFactorization.isProper {m n : ℕ} {g : Matrix (Fin m) (Fin n) ℝ → EReal} (hg : HasAbsolutelyPermutationSymmetricSingularValueFactorization g) : IsProperExtendedRealFunction g

An absolutely permutation symmetric singular-value factorization forces the matrix-valued function to be proper.

class Matrix.IsSymmetricSpectralFunction {m n : ℕ} (g : Matrix (Fin m) (Fin n) ℝ → EReal) : Prop

Definition 7.19: a proper extended-real-valued function on ℝ^(m × n) is symmetric spectral when it is the composition of the singular-value map with some absolutely permutation symmetric proper function on ℝ^(min m n).

• has_absolutely_permutation_symmetric_singular_value_factorization : HasAbsolutelyPermutationSymmetricSingularValueFactorization g

instance Matrix.instIsProperExtendedRealFunctionFinRealOfIsSymmetricSpectralFunction {m n : ℕ} (g : Matrix (Fin m) (Fin n) ℝ → EReal) [hg : IsSymmetricSpectralFunction g] : IsProperExtendedRealFunction g

A symmetric spectral function is proper because its defining singular-value factorization uses an absolutely permutation symmetric associated function.

instance Matrix.instIsSpectralFunctionOfIsSymmetricSpectralFunction {m n : ℕ} {g : Matrix (Fin m) (Fin n) ℝ → EReal} [IsSymmetricSpectralFunction g] : IsSpectralFunction g

A symmetric spectral function is spectral.

theorem Matrix.isSymmetricSpectralFunction_iff_exists_associatedFunction {m n : ℕ} (g : Matrix (Fin m) (Fin n) ℝ → EReal) : IsSymmetricSpectralFunction g ↔ IsProperExtendedRealFunction g ∧ ∃ (f : (Fin (min m n) → ℝ) → EReal), Function.IsAbsolutelyPermutationSymmetric f ∧ g = f ∘ singular_value_function

A function on real m × n matrices is symmetric spectral exactly when it is proper and equals an absolutely permutation symmetric associated function on singular-value coordinates composed with singular_value_function.

instance Matrix.instIsSymmetricSpectralFunctionOfNatEReal {m n : ℕ} : IsSymmetricSpectralFunction fun (x : Matrix (Fin m) (Fin n) ℝ) => 0

The constant zero extended-real-valued function on real m × n matrices is symmetric spectral.