Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 8.2, p. 11 — for A with independent columns, f^A has total curvature at most 1 − 1/κ²(A)

Proved
CurvatureSubmod.CSSP.lemma_8_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

column-subset-selectioncondition-numbercurvaturep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1supermodular

Let AAA be a real m×nm \times nm×n matrix whose columns c1,…,cn∈Rmc_1, \dots, c_n \in \mathbb{R}^mc1​,…,cn​∈Rm are linearly independent, and let

κ(A)=sup⁡∥x∥=1∥Ax∥inf⁡∥x∥=1∥Ax∥\kappa(A) = \frac{\sup_{\|x\|=1}\|Ax\|}{\inf_{\|x\|=1}\|Ax\|}κ(A)=inf∥x∥=1​∥Ax∥sup∥x∥=1​∥Ax∥​

be its condition number. Let fA(S)=∑i=1n∥ci−projS(ci)∥2f^A(S) = \sum_{i=1}^n \|c_i - \mathrm{proj}_S(c_i)\|^2fA(S)=∑i=1n​∥ci​−projS​(ci​)∥2 be the column-subset selection objective, a monotone decreasing set function on [n][n][n]. Then fAf^AfA has total curvature at most 1−1/κ2(A)1 - 1/\kappa^2(A)1−1/κ2(A):

f[n]−jA(j)≤1κ2(A) f∅A(j)for every j∈[n].f^A_{[n]-j}(j) \le \frac{1}{\kappa^2(A)}\, f^A_\emptyset(j) \qquad \text{for every } j \in [n].f[n]−jA​(j)≤κ2(A)1​f∅A​(j)for every j∈[n].

Equivalently, c(fA)=1−min⁡jf[n]−jA(j)/f∅A(j)≤1−1/κ2(A)c(f^A) = 1 - \min_j f^A_{[n]-j}(j)/f^A_\emptyset(j) \le 1 - 1/\kappa^2(A)c(fA)=1−minj​f[n]−jA​(j)/f∅A​(j)≤1−1/κ2(A). The result ties a combinatorial parameter of the column-subset selection objective to the conditioning of the matrix, which is what lets the paper's curvature-dependent guarantees for supermodular minimization be quoted for column-subset selection.

Formalization Note "Non-singular" is read as linearly independent columns, the case in which §8 defines κ(A)\kappa(A)κ(A) as a ratio. Curvature is written in the product form fX−j(j)≤(1−c) f∅(j)f_{X-j}(j) \le (1-c)\,f_\emptyset(j)fX−j​(j)≤(1−c)f∅​(j), which is (1.1) multiplied out for a decreasing function. Under independence the supremum and infimum over the unit sphere are finite and positive, so κ(A)≥1\kappa(A) \ge 1κ(A)≥1 is a genuine real number. For n=0n = 0n=0 there is no jjj and the statement is empty, as on the page.

Preamble
import Mathlib
import Definitions.Def_CurvatureSubmod_CSSP_Setting
Formal statement
namespace CurvatureSubmod.CSSP

/-- Lemma 8.2, p. 11: for `A` with independent columns, `f^A` has total curvature at most
`1 − 1/κ²(A)`, i.e. `f^A_{[n]−j}(j) ≤ (1/κ²(A)) f^A_∅(j)` for every `j` (product form of (1.1)). -/
theorem lemma_8_2 {m n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin m))
    (hc : LinearIndependent ℝ c) :
    CurvatureSubmod.LocalSearch.CurvAtMostDec (fA c) (1 - 1 / condNum c ^ 2) := by sorry

end CurvatureSubmod.CSSP
Source
Sviridenko, Vondrák, Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature (SODA 2015 version, Oct. 9, 2014), p. 11, Lemma 8.2 (proof pp. 11–12), with (1.1) p. 3
Human review
  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me