p. 1040 — the worst-case residual is the same for the largest-singular-value norm
ProvedRobustLS.Unstructured.worst_case_residual_spectralmatrix-normsp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1robust-least-squaresworst-case-residual
Let , , and . If the perturbation bound in (1) is measured in the largest singular value norm instead of the Frobenius norm, the worst-case residual is unchanged:
Since , the spectral ball contains the Frobenius ball; the statement says that the larger ball does not produce a larger worst case.
Formalization Note The maximum is encoded as the supremum of the attained residuals (nonempty and bounded above). The hypothesis excludes the empty system, for which the only perturbation is the empty matrix and the worst case is . The paper normalizes .
Preamble
import Mathlib import Definitions.Def_RobustLS_Unstructured_Core open Matrix
Formal statement
namespace RobustLS.Unstructured
/-- El Ghaoui & Lebret (1997), p. 1040 (PDF p. 6): "the worst-case residual is the same when
the norm used is the largest singular value norm". With `ρ = 1` and `n ≥ 1`, the worst case
over `‖[ΔA Δb]‖ ≤ 1` (largest singular value) is `‖Ax − b‖ + √(‖x‖² + 1)`, the same value as
for the Frobenius ball (Theorem 3.1). The assumption `0 < n` excludes the empty system, where
the only perturbation is the empty matrix and the worst case is `0`. -/
theorem worst_case_residual_spectral {n m : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin m) ℝ)
(b : Fin n → ℝ) (x : Fin m → ℝ) :
worstCaseResidualSpec A b 1 x = eucNorm (A *ᵥ x - b) + Real.sqrt (eucNorm x ^ 2 + 1) := by sorry
end RobustLS.Unstructured
Source
El Ghaoui & Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064 (1997), p. 1040, §3 (remark before §3.1) and Theorem 3.1, proof
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.