talagrand_tangent_sampling_deviation_from_expectation_bound_of_positive_samples

Open

by Minghui · Jun 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

candes-rechtexact-matrix-completionformal-bridgemin-dimensiontalagrandtangent-sampling

This is a formal bridge for the positive-samples Talagrand route from an expectation bound to a single-scale deviation event.

Source: Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 18, Section 4.2, equation (4.8), for the tangent-coordinate estimate; PDF p. 19, Theorem 4.2 and equations (4.9)--(4.10), for the expectation and around-mean deviation structure; Appendix 9.1, PDF p. 46, Theorem 9.1 / equation (9.2), for Talagrand's product-space concentration input.

Mathematical statement: let M be an $n_1\times n_2$ rank- $r$ matrix with SVD data S, let $n=\max(n_1,n_2)$ , and let $p=m/(n_1n_2)$ be the Bernoulli sampling rate. Assume $0<n_1$ , $0<n_2$ , $0<r$ , $0<m\le n_1n_2$ , $1\le\mu_0$ , $1\le\mu_1$ , and $A0(S,\mu_0)$ and $A1(S,\mu_1)$ . If

\mathbb E_p Z(\Omega)\le \mathrm{scale}(C_{\mathrm{expect}},\beta,\mu_0,n,r,m),

then there are positive constants $C,c$ such that

\mathbb P_p\{Z(\Omega)\le \mathrm{scale}(C,\beta,\mu_0,n,r,m)\} \ge 1-c n^{-\beta}.

Here $Z(\Omega)=\mathrm{tangentSamplingDeviation}(\Omega,S,p)$ .

Formalization note: this is a formal bridge, not a new analytic concentration theorem. It composes the source-backed bridge talagrand_tangent_sampling_deviation_around_expectation_of_positive_samples with the source-backed scale-combination theorem sum_tangent_sampling_deviation_scales_le_single_scale and the probability monotonicity theorem bernoulli_tangent_sampling_deviation_bound_probability_mono. The explicit 0 < m hypothesis is deliberate and matches the corrected min-dimension A0 feed used underneath.

Preamble

import Definitions.Def_matrix_completion_tangent

open MatrixCompletion

Formal statement

theorem talagrand_tangent_sampling_deviation_from_expectation_bound_of_positive_samples
    (Cexpect : ℝ) :
    0 < Cexpect →
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧
      ∀ (β : ℝ), 2 < β →
      ∀ (n₁ n₂ r m : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (μ₀ μ₁ : ℝ) (S : SVD M r),
        0 < n₁ → 0 < n₂ → 0 < r → 0 < m → m ≤ n₁ * n₂ →
        1 ≤ μ₀ → 1 ≤ μ₁ →
        A0 S μ₀ → A1 S μ₁ →
        bernoulliExpectation ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
            (fun Omega =>
              tangentSamplingDeviation Omega S
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) ≤
          tangentSamplingDeviationScale Cexpect β μ₀ (max n₁ n₂) r m →
        bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
            (fun Omega =>
              TangentSamplingDeviationBound Omega S
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
                (tangentSamplingDeviationScale C β μ₀ (max n₁ n₂) r m)) ≥
          1 - c * Real.rpow (↑(max n₁ n₂)) (-β) := by sorry

Source

Candes, Emmanuel, and Benjamin Recht. Exact Matrix Completion via Convex Optimization. arXiv:0805.4471 / Foundations of Computational Mathematics 9 (2009), 717--772. Exact locations: PDF p. 18, Section 4.2, equation (4.8); PDF p. 19, Theorem 4.2 and equations (4.9)--(4.10); Appendix 9.1, PDF p. 46, Theorem 9.1 / equation (9.2).

View graph