@[implicit_reducible]

noncomputable def instNormedAddCommGroupMatrixFinReal_firstOrderMethodsOptimization_Beck_2017_1 {m n : ℕ} : NormedAddCommGroup (Matrix (Fin m) (Fin n) ℝ)

The ambient real matrix space is equipped with its Frobenius norm.

@[implicit_reducible]

noncomputable def instNormedSpaceRealMatrixFin_firstOrderMethodsOptimization_Beck_2017_1 {m n : ℕ} : NormedSpace ℝ (Matrix (Fin m) (Fin n) ℝ)

The ambient real matrix space is a normed real vector space.

@[implicit_reducible]

noncomputable def instInnerProductSpaceRealMatrixFin_firstOrderMethodsOptimization_Beck_2017_1 {m n : ℕ} : InnerProductSpace ℝ (Matrix (Fin m) (Fin n) ℝ)

The ambient real matrix space is equipped with its Frobenius inner product.

def orthogonalRectangularDiagonalMapEuclidean {m n : ℕ} (U : ↥(Matrix.orthogonalGroup (Fin m) ℝ)) (V : ↥(Matrix.orthogonalGroup (Fin n) ℝ)) : EuclideanSpace ℝ (Fin (min m n)) → Matrix (Fin m) (Fin n) ℝ

The rectangular diagonal reconstruction map with a Euclidean singular-value vector input.

theorem matrixSpectralLift_proper_closed_convex {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (hf_symm : Function.IsAbsolutelyPermutationSymmetric f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) : IsProperExtendedRealFunction (f ∘ singular_value_function) ∧ LowerSemicontinuous (f ∘ singular_value_function) ∧ is_convex_function (f ∘ singular_value_function)

Helper for Theorem 7.7: the matrix spectral lift of an absolutely permutation symmetric, closed, convex profile is proper, closed, and convex on the ambient matrix space.

theorem proximal_objective_matrixSpectralLift_orthogonal_rectangular_eq {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (U : ↥(Matrix.orthogonalGroup (Fin m) ℝ)) (V : ↥(Matrix.orthogonalGroup (Fin n) ℝ)) (d : Fin (min m n) → ℝ) (Z : Matrix (Fin m) (Fin n) ℝ) : proximal_objective (f ∘ singular_value_function) (orthogonalRectangularDiagonalMap U V d) Z = proximal_objective (f ∘ singular_value_function) (rectangularDiagonal d) ((↑U).transpose * Z * ↑V)

Helper for Theorem 7.7: orthogonal transport normalizes the matrix spectral proximal objective to the rectangular diagonal basis.

theorem frobenius_norm_rectangularDiagonal_eq_toLp {m n : ℕ} (x : Fin (min m n) → ℝ) : ‖rectangularDiagonal x‖ = ‖WithLp.toLp 2 x‖

Helper for Theorem 7.7: the Frobenius norm of a rectangular diagonal matrix is the Euclidean L² norm of its diagonal profile.

theorem mem_prox_matrixSpectralLift_orthogonal_rectangular_iff {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (U : ↥(Matrix.orthogonalGroup (Fin m) ℝ)) (V : ↥(Matrix.orthogonalGroup (Fin n) ℝ)) (d : Fin (min m n) → ℝ) (Z : Matrix (Fin m) (Fin n) ℝ) : Z ∈ prox[f ∘ singular_value_function] (orthogonalRectangularDiagonalMap U V d) ↔ (↑U).transpose * Z * ↑V ∈ prox[f ∘ singular_value_function] (rectangularDiagonal d)

Helper for Theorem 7.7: proximal membership is invariant under orthogonal transport to the rectangular diagonal basis.

def row_coordinate_sign_pattern {m n : ℕ} (i : Fin (min m n)) : Fin m → ℝ

Helper for Theorem 7.7: the row-side sign pattern that flips only the common-diagonal coordinate i.

def column_coordinate_sign_pattern {m n : ℕ} (i : Fin (min m n)) : Fin n → ℝ

Helper for Theorem 7.7: the column-side sign pattern that flips only the common-diagonal coordinate i.

theorem rowCoordinateSignFlip_mem_orthogonalGroup {m n : ℕ} (i : Fin (min m n)) : Matrix.diagonal (row_coordinate_sign_pattern i) ∈ Matrix.orthogonalGroup (Fin m) ℝ

Helper for Theorem 7.7: the row-side coordinate sign pattern defines an orthogonal matrix.

noncomputable def rowCoordinateSignFlip {m n : ℕ} (i : Fin (min m n)) : ↥(Matrix.orthogonalGroup (Fin m) ℝ)

Helper for Theorem 7.7: the row-side coordinate sign pattern defines an orthogonal matrix.

theorem columnCoordinateSignFlip_mem_orthogonalGroup {m n : ℕ} (i : Fin (min m n)) : Matrix.diagonal (column_coordinate_sign_pattern i) ∈ Matrix.orthogonalGroup (Fin n) ℝ

Helper for Theorem 7.7: the column-side coordinate sign pattern defines an orthogonal matrix.

noncomputable def columnCoordinateSignFlip {m n : ℕ} (i : Fin (min m n)) : ↥(Matrix.orthogonalGroup (Fin n) ℝ)

Helper for Theorem 7.7: the column-side coordinate sign pattern defines an orthogonal matrix.

theorem pairedCoordinateSignFlip_conjugate_apply {m n : ℕ} (i : Fin (min m n)) (W : Matrix (Fin m) (Fin n) ℝ) (j : Fin m) (k : Fin n) : (↑(rowCoordinateSignFlip i) * W * (↑(columnCoordinateSignFlip i)).transpose) j k = row_coordinate_sign_pattern i j * W j k * column_coordinate_sign_pattern i k

Helper for Theorem 7.7: paired row/column coordinate sign flips act entrywise by multiplying the corresponding row and column signs.

theorem pairedCoordinateSignFlip_fixes_rectangularDiagonal {m n : ℕ} (i : Fin (min m n)) (d : Fin (min m n) → ℝ) : orthogonalRectangularDiagonalMap (rowCoordinateSignFlip i) (columnCoordinateSignFlip i) d = rectangularDiagonal d

Helper for Theorem 7.7: the paired coordinate sign flips fix every rectangular diagonal matrix.

theorem eq_rectangularDiagonal_of_fixed_by_pairedCoordinateSignFlip {m n : ℕ} (W : Matrix (Fin m) (Fin n) ℝ) (hfix : ∀ (i : Fin (min m n)), ↑(rowCoordinateSignFlip i) * W * (↑(columnCoordinateSignFlip i)).transpose = W) : ∃ (w : Fin (min m n) → ℝ), W = rectangularDiagonal w

Helper for Theorem 7.7: if a rectangular matrix is fixed by every paired row/column coordinate sign flip, then it is rectangular diagonal.

theorem rectangular_basis_prox_is_rectangularDiagonal {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (hf_symm : Function.IsAbsolutelyPermutationSymmetric f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (d : Fin (min m n) → ℝ) {W : Matrix (Fin m) (Fin n) ℝ} (hW : W ∈ prox[f ∘ singular_value_function] (rectangularDiagonal d)) : ∃ (w : Fin (min m n) → ℝ), W = rectangularDiagonal w

Helper for Theorem 7.7: every proximal point at a rectangular diagonal base matrix is itself a rectangular diagonal matrix.

theorem rectangularDiagonal_mem_prox_euclidean_of_mem_prox_matrixSpectralLift {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (hf_symm : Function.IsAbsolutelyPermutationSymmetric f) (d w : Fin (min m n) → ℝ) (hdiag : rectangularDiagonal w ∈ prox[f ∘ singular_value_function] (rectangularDiagonal d)) : WithLp.toLp 2 w ∈ prox[fun (y : EuclideanSpace ℝ (Fin (min m n))) => f y.ofLp] (WithLp.toLp 2 d)

Helper for Theorem 7.7: a rectangular diagonal proximal point in the matrix problem induces the corresponding Euclidean proximal point of the vector profile.

theorem prox_matrixSpectralLift_eq_image_orthogonalRectangularDiagonalMap {m n : ℕ} (f : (Fin (min m n) → ℝ) → EReal) (hf_symm : Function.IsAbsolutelyPermutationSymmetric f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (X : Matrix (Fin m) (Fin n) ℝ) (U : ↥(Matrix.orthogonalGroup (Fin m) ℝ)) (V : ↥(Matrix.orthogonalGroup (Fin n) ℝ)) (hsvd : X = orthogonalRectangularDiagonalMap U V (singular_value_function X)) : prox[f ∘ singular_value_function] X = orthogonalRectangularDiagonalMapEuclidean U V '' prox[fun (y : EuclideanSpace ℝ (Fin (min m n))) => f y.ofLp] (WithLp.toLp 2 (singular_value_function X))

Theorem 7.7: if f : ℝ^(min(m,n)) → (-∞, ∞] is absolutely permutation symmetric, closed, and convex, and if X = U * rectangularDiagonal (singular_value_function X) * Vᵀ, then the proximal set of the matrix spectral lift f ∘ singular_value_function at X is the orthogonal image of the Euclidean vector proximal set of f at σ(X) = singular_value_function X. The vector-side proximal problem is stated on EuclideanSpace ℝ (Fin (min m n)), matching the Frobenius geometry of rectangular diagonal matrices.

theorem prox_matrixSpectralLift_eq_singleton_orthogonalRectangularDiagonalMap {m n : ℕ} {f : (Fin (min m n) → ℝ) → EReal} (hf_symm : Function.IsAbsolutelyPermutationSymmetric f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) {X : Matrix (Fin m) (Fin n) ℝ} {U : ↥(Matrix.orthogonalGroup (Fin m) ℝ)} {V : ↥(Matrix.orthogonalGroup (Fin n) ℝ)} (hsvd : X = orthogonalRectangularDiagonalMap U V (singular_value_function X)) {x : EuclideanSpace ℝ (Fin (min m n))} (hprox : prox[fun (y : EuclideanSpace ℝ (Fin (min m n))) => f y.ofLp] (WithLp.toLp 2 (singular_value_function X)) = {x}) : prox[f ∘ singular_value_function] X = {orthogonalRectangularDiagonalMapEuclidean U V x}

If the Euclidean vector proximal set of f at the singular-value vector of X is the singleton {x}, then the proximal set of the matrix spectral lift at X is the singleton {U * rectangularDiagonal x.ofLp * Vᵀ}.