inner_sign_average_khintchine_variance_proxy_bound

Disproved

by Hartmann_Psi · Jun 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

khintchinematrix-completionrudelson-selection

Pointwise (fixed observation set) matrix Khintchine bound with Rudelson variance proxy: the Rademacher sign-average of the centered selected rank-one tangent Gram operator is at most a universal constant times sqrt(log(max n1 n2)) times the coordinate radius R times the square root of the sampled Gram operator norm. Assembled from the matrix 2p-moment Khintchine inequality, reindexing, the Rudelson/Loewner variance proxy, and the dimension-window collapse. (Candes-Recht 2009, Section 9.1; Rudelson 1999.)

Preamble

import Definitions.Def_matrix_completion_tangent
import Definitions.Def_matrix_completion_bernoulli
import Mathlib.Analysis.CStarAlgebra.Matrix
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Complex.ExponentialBounds
open MatrixCompletion
open scoped Classical BigOperators Matrix Matrix.Norms.L2Operator

Formal statement

theorem inner_sign_average_khintchine_variance_proxy_bound :
    ∃ Csym0 : ℝ, 0 < Csym0 ∧
      ∀ (n₁ n₂ r m : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (S : SVD M r) (R : ℝ),
        0 < n₁ → 0 < n₂ → 0 < r → m ≤ n₁ * n₂ →
        0 ≤ R →
        (∀ i : Fin n₁, ∀ j : Fin n₂,
          frobeniusNorm (tangentProjection S (coordinateMatrix i j)) ≤ R) →
        ∀ (Omega : Finset (Fin n₁ × Fin n₂)),
        (∑ Es : Finset (Fin n₁ × Fin n₂),
            ((1:ℝ)/2) ^ (Fintype.card (Fin n₁ × Fin n₂)) *
              ‖(LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin
                (∑ ab : Fin n₁ × Fin n₂,
                  (((if ab ∈ Es then (1:ℝ) else -1) *
                      (if ab ∈ Omega then (1:ℝ) else 0)) •
                    Matrix.vecMulVec
                      (fun e : Fin n₁ × Fin n₂ => tangentProjection S (coordinateMatrix ab.1 ab.2) e.1 e.2)
                      (fun e : Fin n₁ × Fin n₂ => tangentProjection S (coordinateMatrix ab.1 ab.2) e.1 e.2)))))‖)
          ≤ Csym0 *
              (Real.sqrt (Real.log (↑(max n₁ n₂))) * R) *
              Real.sqrt
                ‖(LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin
                  (∑ ab : Fin n₁ × Fin n₂,
                    (if ab ∈ Omega then (1:ℝ) else 0) •
                      Matrix.vecMulVec
                        (fun e : Fin n₁ × Fin n₂ => tangentProjection S (coordinateMatrix ab.1 ab.2) e.1 e.2)
                        (fun e : Fin n₁ × Fin n₂ => tangentProjection S (coordinateMatrix ab.1 ab.2) e.1 e.2))))‖ := by sorry

Source

Candes, Recht, Exact Matrix Completion via Convex Optimization (2009), Section 9.1

View graph