Prove2Me

(2.11) — the inequality deduced from (2.8) for every A∈AA\in\mathbb A with support (S1,S2)(S_1,S_2)

Proved
KLTNuclear.Oracle.eq_2_11

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

matrix-estimationnuclear-normoracle-inequalityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Work in the trace regression model E(Yi∣Xi)=⟨A0,Xi⟩\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle with square-integrable design entries and integrable responses. Let A\mathbb A be a convex set of m1×m2m_1\times m_2 matrices, λ>0\lambda>0, and fix a realization of the sample at which A^λ\hat A^\lambda minimizes LnL_n over A\mathbb A; let M=1n∑i(YiXi−E(YiXi))\mathbf M=\frac1n\sum_i(Y_iX_i-\mathbb E(Y_iX_i)). Then for every A∈AA\in\mathbb A with singular value decomposition A=∑j=1rσjujvj⊤A=\sum_{j=1}^r\sigma_ju_jv_j^\top and support (S1,S2)(S_1,S_2),

∥A^λ−A0∥L2(Π)2+∥A^λ−A∥L2(Π)2+λ∥PS1⊥A^λPS2⊥∥1≤∥A−A0∥L2(Π)2+λ∥PS1(A^λ−A)PS2∥1+2⟨M,A^λ−A⟩.\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}+\|\hat A^\lambda-A\|^2_{L_2(\Pi)}+\lambda\|P_{S_1^\perp}\hat A^\lambda P_{S_2^\perp}\|_1\le\|A-A_0\|^2_{L_2(\Pi)}+\lambda\|P_{S_1}(\hat A^\lambda-A)P_{S_2}\|_1+2\langle\mathbf M,\hat A^\lambda-A\rangle .

This is the key deterministic inequality of the fast-rate part of Theorem 1; no relation between λ\lambda and ∥M∥∞\|\mathbf M\|_\infty is needed for it.

Formalization Note Model hypothesis in conditional-expectation form; integrability conditions added; independence not assumed. The support is given by SVD data S : SVD A r.

Preamble
import Mathlib
import Definitions.Def_KLTNuclear_Oracle_Model

open MeasureTheory MatrixCompletion
Formal statement
namespace KLTNuclear.Oracle

/-- (2.11) (p. 8): for a convex 𝔸 and every A ∈ 𝔸 with support (S₁, S₂). -/
theorem eq_2_11 {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {n m₁ m₂ : ℕ} (hn : 0 < n)
    (X : Fin n → Ω → RealMatrix m₁ m₂) (Y : Fin n → Ω → ℝ)
    (hreg : SampleRegularity P X Y)
    (A₀ : RealMatrix m₁ m₂) (hmodel : TraceRegressionModel P X Y A₀)
    (𝔸 : Set (RealMatrix m₁ m₂)) (h𝔸 : Convex ℝ 𝔸) (lam : ℝ) (hlam : 0 < lam)
    (ω : Ω) (Ahat : RealMatrix m₁ m₂) (hAhat : IsEstimator P X Y lam ω 𝔸 Ahat) :
    ∀ A ∈ 𝔸, ∀ (r : ℕ) (S : SVD A r),
      l2NormSq P X (Ahat - A₀) + l2NormSq P X (Ahat - A) + lam * nuclearNorm (normalProjection S Ahat) ≤
        l2NormSq P X (A - A₀) + lam * nuclearNorm (twoSidedSingularProjection S (Ahat - A)) +
          2 * matrixInner (noiseMatrix P X Y ω) (Ahat - A) := by sorry

end KLTNuclear.Oracle
Source
Koltchinskii, Lounici, Tsybakov, Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion, arXiv:1011.6256v4, p. 8, (2.11)
Human review

  • Endorsed by Shuze Chen · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 7, 2026

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

View graph