§3.1, Eq. (16) — the worst-case residual is at most ‖Ax − b‖ + √(‖x‖² + 1)
ProvedRobustLS.Unstructured.worst_case_residual_upper_boundp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1robust-least-squaresworst-case-residual
Let , and , with Euclidean norms on vectors. For every perturbation , whose augmented matrix has Frobenius norm ,
Taking the maximum over all such perturbations gives the upper bound (16), , the first half of the closed form in Theorem 3.1.
Formalization Note The bound is stated perturbation by perturbation rather than for the sSup defining , so that it cannot hold for the vacuous reason that a supremum of an unbounded set is in Lean. The paper normalizes .
Preamble
import Mathlib import Definitions.Def_RobustLS_Unstructured_Core open Matrix
Formal statement
namespace RobustLS.Unstructured
/-- El Ghaoui & Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data,
SIAM J. Matrix Anal. Appl. 18(4) (1997), Theorem 3.1, proof, Eq. (16), p. 1040 (PDF p. 6):
`r(A, b, x) ≤ ‖Ax − b‖ + √(‖x‖² + 1)` (with `ρ = 1`). Stated perturbation by perturbation:
every `[ΔA Δb]` with Frobenius norm at most `1` gives a residual at most the bound. -/
theorem worst_case_residual_upper_bound {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℝ)
(b : Fin n → ℝ) (x : Fin m → ℝ) (ΔA : Matrix (Fin n) (Fin m) ℝ) (Δb : Fin n → ℝ)
(hΔ : frobNorm (augment ΔA Δb) ≤ 1) :
perturbedResidual A b ΔA Δb 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, Theorem 3.1, proof, Eq. (16)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.