rudelson_selection_expected_tangent_deviation_from_coordinate_radius_bound_dense

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Corrected (sampling-density) variant of rudelson_selection_expected_tangent_deviation_from_coordinate_radius_bound (which is FALSE without a density hypothesis). Rudelson's selection estimate (Candès–Recht 2009, Thm 4.2, eq 4.9): there is a universal constant $C_{sel}>0$ such that for every $\beta>2$ and every rank-$r$ matrix with a coordinate radius bound $\|P_T(e_ie_j^*)\|_F\le R$, provided the sampling density satisfies $m \ge \beta\,(\max n_1 n_2)\,r\,\log(\max n_1 n_2)$, the expected tangent sampling deviation $\mathbb{E}\,p^{-1}\|P_TP_\Omega P_T-pP_T\|$ is at most $C_{sel}\,\sqrt{\log(\max n_1 n_2)/p}\,R$ where $p=m/(n_1n_2)$. The density hypothesis (the paper's 'provided $C_R\sqrt{\mu_0 n r\beta\log n/m}<1$' condition) is what excludes the maximal-coherence low-sample counterexample that disproved the un-hypothesized form.

Why this node was retired

The posted statement is

theorem rudelson_selection_expected_tangent_deviation_from_coordinate_radius_bound_dense :
    ∃ Csel : ℝ, 0 < Csel ∧
      ∀ (β : ℝ), 2 < β →
      ∀ (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 →
        (m : ℝ) ≥ β * (↑(max n₁ n₂)) * (r : ℝ) *
          Real.log (↑(max n₁ n₂)) →
        (∀ i : Fin n₁, ∀ j : Fin n₂,
          frobeniusNorm (tangentProjection S (coordinateMatrix i j)) ≤ R) →
        bernoulliExpectation ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
            (fun Omega =>
              tangentSamplingDeviation Omega S
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) ≤
          Csel *
            Real.sqrt
              (Real.log (↑(max n₁ n₂)) /
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
            R := by sorry

The source square-root expected-deviation/concentration rate has a smallness or density proviso, omitted here; sparse coherent examples have deviations of order 1/p.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Restore the source proviso that the proposed deviation scale is <1 (with positive sampling rate and valid Bernoulli probabilities), equivalently a sufficiently strong density floor m>C²μ₀nrβlog n for the scale C√(μ₀nrβlog n/m). For a coordinate-radius formulation require its own scale C R√(log n/p)<1, not merely a floor on R. Recheck constants and rectangular dimensions separately.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.