Theorem 23.8 (Candès): for ε < 1/(1+√2) and W (ε,2s)-RIP, the ℓ₁-minimizer x⋆ with Wx⋆ = Wx has ‖x⋆ − x‖₂ ≤ 2(1+ρ)/(1−ρ) s^{−1/2}‖x − x_s‖₁, ρ = √2ε/(1−ε)

import Definitions.Def_UnderstandingML_DimReduction

open MeasureTheory ProbabilityTheory

namespace UnderstandingML

/-- **Theorem 23.8 (Candès 2008)** (p. 332). Let `ε < 1/(1 + √2)` and let `W` be an
`(ε, 2s)`-RIP matrix. Let `x` be an arbitrary vector and denote `x_s ∈ argmin_{v : ‖v‖₀ ≤ s} ‖x − v‖₁`
(the vector which equals `x` on the `s` largest elements of `x` and `0` elsewhere). Let `y = Wx`
and let `x⋆ ∈ argmin_{v : Wv = y} ‖v‖₁` be the reconstructed vector. Then
`‖x⋆ − x‖₂ ≤ 2 (1 + ρ)/(1 − ρ) s^{−1/2} ‖x − x_s‖₁`, where `ρ = √2 ε/(1 − ε)`. `s ≥ 1`. -/
theorem rip_l1_recovery {n d s : ℕ} (hs : 0 < s) (ε : ℝ) (hε0 : 0 ≤ ε)
    (hε : ε < 1 / (1 + Real.sqrt 2)) (W : Matrix (Fin n) (Fin d) ℝ) (hW : IsRIP ε (2 * s) W)
    (x xs xstar : Fin d → ℝ) (hxs : l0Norm xs ≤ s)
    (hxs_min : ∀ v, l0Norm v ≤ s → l1Norm (x - xs) ≤ l1Norm (x - v))
    (hy : W.mulVec xstar = W.mulVec x)
    (hmin : ∀ v, W.mulVec v = W.mulVec x → l1Norm xstar ≤ l1Norm v) :
    Real.sqrt (sqNorm (xstar - x)) ≤
      2 * (1 + Real.sqrt 2 * ε / (1 - ε)) / (1 - Real.sqrt 2 * ε / (1 - ε)) *
        (s : ℝ) ^ (-(1 : ℝ) / 2) * l1Norm (x - xs) := by sorry

end UnderstandingML

• Endorsed by Shuze Chen · Sep 25, 2026

  Confirmed by the moderator at approval.

• Endorsed by naimengye · Sep 25, 2026

  Confirmed by the mission captain (proposal self-audit).