matrix_khintchine_log_window_dimension_factor

Proved

by Minghui · Jun 25, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

This is the scalar dimension-window bridge for the Rudelson/Lust-Picquard noncommutative-Khintchine step in the Candes--Recht tangent-sampling estimate.

Source: Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 19, Section 4.2, Theorem 4.2, equation (4.9), where the expectation estimate has the $sqrt(log n)$ scale; Rudelson, Random vectors in the isotropic position, JFA 164 (1999), Theorem 1, proof Steps 1--2; and the standard moment-window optimization in the noncommutative Khintchine inequality.

Mathematical statement. There is a universal constant $C_win > 0$ such that for every matrix dimension $d$ and ambient dimension parameter $N$ , if

0 < d, 2 <= N, d <= N^2,

then one can choose an integer moment parameter $q >= 1$ with

sqrt(2q) d^(1/(2q)) <= C_win sqrt(log N).

Variables and notation. In the downstream matrix-completion route, $N = n = max(n_1,n_2)$ and $d$ is the Hilbert-space dimension after vectorization, with $d <= n^2$ . The Bernoulli sampling rate is $p = m/(n_1 n_2)$ and $Omega$ is a fixed Bernoulli sample realization, but this scalar bridge does not itself quantify over $p$ or $Omega$ .

Formalization note. This is a formal bridge. It does not appear verbatim in Candes--Recht. It bridges the source-backed parent/import theorem rademacher_matrix_operator_norm_2p_moment_bound (0cafa5a3) to the source-backed child route through rademacher_matrix_operator_norm_first_moment_log_window_from_2p (136263d8) and inner_sign_average_khintchine_variance_proxy_bound_of_two_le_max (f4806ebd). The explicit hypothesis $2 <= N$ is inherited from the corrected f4806ebd route and avoids the deprecated $N = 1$ defect.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open scoped Classical BigOperators

Formal statement

theorem matrix_khintchine_log_window_dimension_factor :
    ∃ Cwin : ℝ, 0 < Cwin ∧
      ∀ {d N : ℕ}, 0 < d → 2 ≤ N → d ≤ N * N →
        ∃ p : ℕ, 1 ≤ p ∧
          Real.sqrt (2 * (p : ℝ)) *
              (d : ℝ) ^ ((1 : ℝ) / (2 * (p : ℝ))) ≤
            Cwin * Real.sqrt (Real.log (N : ℝ)) := by
  sorry

Source

Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 19, Section 4.2, Theorem 4.2, equation (4.9); Rudelson, Random vectors in the isotropic position, JFA 164 (1999), Theorem 1, proof Steps 1--2; Lust-Picquard/Pisier noncommutative Khintchine moment-window optimization.

View graph