Lemma 8.2, p. 11 — for A with independent columns, f^A has total curvature at most 1 − 1/κ²(A)
ProvedCurvatureSubmod.CSSP.lemma_8_2Let be a real matrix whose columns are linearly independent, and let
be its condition number. Let be the column-subset selection objective, a monotone decreasing set function on . Then has total curvature at most :
Equivalently, . 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 as a ratio. Curvature is written in the product form , 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 is a genuine real number. For there is no and the statement is empty, as on the page.
import Mathlib import Definitions.Def_CurvatureSubmod_CSSP_Setting
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.