Prove2Me

(2.17) — the bound combining (2.11), (2.12), (2.16) and Assumption 1

Proved
KLTNuclear.Oracle.eq_2_17

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 satisfying Assumption 1 with constant μ>0\mu>0 (∥D∥L2(Π)2≥μ−2∥D∥22\|D\|^2_{L_2(\Pi)}\ge\mu^{-2}\|D\|_2^2 for D∈A−AD\in\mathbb A-\mathbb A), let λ>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)). 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), with

Λ=2∥PA(M)∥2,Γ=2∥PS1⊥MPS2⊥∥∞,\Lambda=2\|\mathcal P_A(\mathbf M)\|_2,\qquad\Gamma=2\|P_{S_1^\perp}\mathbf MP_{S_2^\perp}\|_\infty,

one has

∥A^λ−A0∥L2(Π)2+∥A^λ−A∥L2(Π)2+λ∥PS1⊥A^λPS2⊥∥1≤∥A−A0∥L2(Π)2+μ(λrank⁡(A)+Λ)∥A^λ−A∥L2(Π)+Γ∥PS1⊥A^λPS2⊥∥1.\|\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)}+\mu\big(\lambda\sqrt{\operatorname{rank}(A)}+\Lambda\big)\|\hat A^\lambda-A\|_{L_2(\Pi)}+\Gamma\|P_{S_1^\perp}\hat A^\lambda P_{S_2^\perp}\|_1 .

It is the last intermediate inequality of the proof of Theorem 1 before the fast-rate bounds (2.4) and (2.5).

Formalization Note ∥⋅∥L2(Π)\|\cdot\|_{L_2(\Pi)} is the square root of ∥⋅∥L2(Π)2\|\cdot\|^2_{L_2(\Pi)}. Model hypothesis in conditional-expectation form; integrability conditions added; independence not assumed.

Preamble
import Mathlib
import Definitions.Def_KLTNuclear_Oracle_Model

open MeasureTheory MatrixCompletion
Formal statement
namespace KLTNuclear.Oracle

/-- (2.17) (p. 9): for a convex 𝔸 under Assumption 1 with constant μ, every A ∈ 𝔸 with
support (S₁, S₂), Λ = 2‖𝒫_A(𝐌)‖₂ and Γ = 2‖P_{S₁⊥} 𝐌 P_{S₂⊥}‖∞. -/
theorem eq_2_17 {Ω : 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 ℝ 𝔸) (μ : ℝ) (hμ : Assumption1 P X 𝔸 μ)
    (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 * Real.sqrt (A.rank : ℝ) +
              2 * frobeniusNorm (tangentProjection S (noiseMatrix P X Y ω))) * l2Norm P X (Ahat - A) +
          2 * spectralNorm (normalProjection S (noiseMatrix P X Y ω)) *
            nuclearNorm (normalProjection S Ahat) := 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. 9, (2.17)
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