On $\mathbb C$ , $\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|$ when $\theta^*\in\mathcal M$ (Section 2.4, p. 10)

Proved

UnifiedMEstimator.General.section24_regularizer_bound_on_C

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

high-dimensional-statisticsm-estimatorp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $E$ be a finite-dimensional real inner product space, $\mathcal R$ a norm on $E$ , and $\mathcal M\subseteq\overline{\mathcal M}$ subspaces of $E$ . Write $\Delta_S$ for the orthogonal projection of $\Delta$ onto a subspace $S$ , $\Psi$ for the subspace compatibility constant and $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ for the set of Eq. (17).

Suppose that $\theta^*\in\mathcal M$ and $\Delta\in\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ . Then $\mathcal R(\Delta_{\overline{\mathcal M}^\perp})\le3\,\mathcal R(\Delta_{\overline{\mathcal M}})$ , and

\mathcal R(\Delta)\le\mathcal R(\Delta_{\overline{\mathcal M}^\perp})+\mathcal R(\Delta_{\overline{\mathcal M}})\le4\,\mathcal R(\Delta_{\overline{\mathcal M}})\le4\,\Psi(\overline{\mathcal M})\,\|\Delta\| .

This is the step at which the compatibility constant $\Psi(\overline{\mathcal M})$ enters the analysis: on the set $\mathbb C$ the regularizer is controlled by the error norm. It is used to derive restricted strong convexity from bounds of the form (20), and the same comparison appears in the error bound of Theorem 1.

Formalization Note The paper's display is a chain; each link is a separate conjunct. The standing assumption $\mathcal M\subseteq\overline{\mathcal M}$ of Section 2.2 is a hypothesis; decomposability is not needed for this step and is not assumed.

Preamble

import Mathlib
import Definitions.Def_UnifiedMEstimator_General_Core

Formal statement

namespace UnifiedMEstimator.General

/-- Section 2.4, p. 10, first display: if `θ* ∈ M` (with `M ⊆ M̄`), then every `Δ` in
`C(M, M̄⊥; θ*)` satisfies `R(Δ_{M̄⊥}) ≤ 3R(Δ_{M̄})` and
`R(Δ) ≤ R(Δ_{M̄⊥}) + R(Δ_{M̄}) ≤ 4R(Δ_{M̄}) ≤ 4Ψ(M̄)‖Δ‖`. -/
theorem section24_regularizer_bound_on_C
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (R : E → ℝ) (M Mbar : Submodule ℝ E) (θstar Δ : E)
    (hR : IsNormFn R) (hle : M ≤ Mbar) (hθ : θstar ∈ M)
    (hΔ : Δ ∈ setC R M Mbar θstar) :
    R (Mbarᗮ.starProjection Δ) ≤ 3 * R (Mbar.starProjection Δ) ∧
    R Δ ≤ R (Mbarᗮ.starProjection Δ) + R (Mbar.starProjection Δ) ∧
    R (Mbarᗮ.starProjection Δ) + R (Mbar.starProjection Δ) ≤ 4 * R (Mbar.starProjection Δ) ∧
    4 * R (Mbar.starProjection Δ) ≤ 4 * compat R Mbar * ‖Δ‖ := by sorry

end UnifiedMEstimator.General

Source

Negahban, Ravikumar, Wainwright and Yu, A Unified Framework for High-Dimensional Analysis of M-Estimators with Decomposable Regularizers, arXiv:1010.2731v3, p. 10, Section 2.4, first display

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $E$ is any finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and induced norm $\|\cdot\|$ . Write $P_S$ for orthogonal projection onto a subspace $S$ and $S^\perp$ for its orthogonal complement. The theorem takes:

a function $R : E \to \mathbb{R}$ ;
linear subspaces $M$ and $\bar M$ of $E$ ;
vectors $\theta^*$ and $\Delta$ in $E$ .

Hypotheses.

$R$ is a norm: it is nonnegative, $R(x) = 0$ exactly when $x = 0$ , $R(cx) = |c|R(x)$ , and $R(x+y) \le R(x) + R(y)$ .
$M \subseteq \bar M$ .
$\theta^* \in M$ .
$\Delta$ satisfies

R(P_{\bar M^\perp}\Delta) \le 3R(P_{\bar M}\Delta) + 4R(P_{M^\perp}\theta^*).

No decomposability of $R$ is assumed.

Conclusion. All four of the following hold:

R(P_{\bar M^\perp}\Delta) \le 3R(P_{\bar M}\Delta),

R(\Delta) \le R(P_{\bar M^\perp}\Delta) + R(P_{\bar M}\Delta),

R(P_{\bar M^\perp}\Delta) + R(P_{\bar M}\Delta) \le 4R(P_{\bar M}\Delta),

4R(P_{\bar M}\Delta) \le 4\,\Psi(\bar M)\,\|\Delta\|.

Here

\Psi(\bar M) = \sup\{R(u)/\|u\| : u \in \bar M,\ u \ne 0\},

where the supremum is $0$ if the set is empty or unbounded above.

Degenerate cases.

$\bar M = \{0\}$ . Then $M = \{0\}$ and $\theta^* = 0$ . Hypothesis 4 reads $R(\Delta) \le 0$ , which forces $\Delta = 0$ , and every quantity in the conclusion is $0$ . Since $\Psi(\{0\}) = 0$ by the empty-set convention, the last inequality reads $0 \le 0$ .
$E = \{0\}$ . Everything is $0$ .
$\bar M = E$ . Then $P_{\bar M^\perp}\Delta = 0$ and hypothesis 4 holds for every $\Delta$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

On C\mathbb CC, R(Δ)≤4Ψ(M‾)∥Δ∥\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|R(Δ)≤4Ψ(M)∥Δ∥ when θ∗∈M\theta^*\in\mathcal Mθ∗∈M (Section 2.4, p. 10)

On $\mathbb C$ , $\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|$ when $\theta^*\in\mathcal M$ (Section 2.4, p. 10)