Successive projection algorithm

StructureSeparable data matrix#✓fully proved

A separable data matrix: columns m j are sub-convex combinations of r linearly independent archetypes w k, and every archetype is a column (Gillis–Vavasis Assumption 1).

Cslib.MachineLearning.MatrixFactorization.SuccessiveProjection.Separable · 15 lines

structure Separable (m : ι → E) (r : ℕ) where
  /-- The archetypes (columns of `W`). -/
  w : Fin r → E
  /-- The mixing weights (entries of `H`). -/
  h : Fin r → ι → ℝ
  /-- The archetypes are linearly independent (`W` has full column rank). -/
  linearIndependent : LinearIndependent ℝ w
  /-- The mixing weights are nonnegative. -/
  nonneg : ∀ k j, 0 ≤ h k j
  /-- Each column's weights sum to at most one. -/
  sum_le_one : ∀ j, ∑ k, h k j ≤ 1
  /-- Each column is the corresponding combination of the archetypes. -/
  eq_sum : ∀ j, m j = ∑ k, h k j • w k
  /-- Every archetype is one of the columns (separability). -/
  pure : ∀ k, ∃ j, m j = w k

Used by 3

Used bySPA recovers archetypes · SPA recovers archetypes · Successive projection finds every archetype after r picks

DefinitionResidual of a column in the successive projection algorithm#✓fully proved

The residual of column j: its projection onto the orthogonal complement of the span of the columns indexed by S.

noncomputable def residual (m : ι → E) (S : Finset ι) (j : ι) : E :=
  haveI := Classical.decEq E
  m j - (Submodule.span ℝ ((S.image m : Finset E) : Set E)).starProjection (m j)

Used by 4

Used byExistence of successive projection runs of every length · Run of the successive projection algorithm · SPA recovers archetypes · SPA recovers archetypes

DefinitionRun of the successive projection algorithm#✓fully proved

S (most recent pick first) is a run of the successive projection algorithm: each pick maximizes the residual norm given the earlier picks (ties broken arbitrarily).

def IsSPARun (m : ι → E) : List ι → Prop
  | [] => True
  | j :: S => IsSPARun m S ∧ ∀ i, ‖residual m S.toFinset i‖ ≤ ‖residual m S.toFinset j‖

Uses 1 · Used by 4

Statement usesResidual of a column in the successive projection algorithm

Used byExistence of successive projection runs of every length · SPA recovers archetypes · SPA recovers archetypes · Successive projection finds every archetype after r picks

TheoremNorm bound for a sub-convex combination of vectors#✓fully proved

Gillis–Vavasis Lemma 1 (f = ‖·‖²), bound: a sub-convex combination of vectors of norm at most M has norm at most M.

theorem norm_sum_smul_le {r : ℕ} (w : Fin r → E) (h : Fin r → ℝ) {M : ℝ} (hM : 0 ≤ M)
    (hw : ∀ k, ‖w k‖ ≤ M) (hh : ∀ k, 0 ≤ h k) (hsum : ∑ k, h k ≤ 1) :
    ‖∑ k, h k • w k‖ ≤ M

Used by 2

Used bySPA recovers archetypes · SPA recovers archetypes

TheoremEquality case of the sub-convex combination norm bound#✓fully proved

Gillis–Vavasis Lemma 1 (f = ‖·‖²), equality case: for linearly independent vectors of norm at most M > 0, a sub-convex combination of norm M is a vertex w k with ‖w k‖ = M.

theorem eq_single_of_norm_sum_smul_eq {r : ℕ} {w : Fin r → E} (hli : LinearIndependent ℝ w)
    (h : Fin r → ℝ) {M : ℝ} (hM : 0 < M) (hw : ∀ k, ‖w k‖ ≤ M) (hh : ∀ k, 0 ≤ h k)
    (hsum : ∑ k, h k ≤ 1) (heq : ‖∑ k, h k • w k‖ = M) :
    ∃ k, h = Pi.single k 1 ∧ ‖w k‖ = M

TheoremSPA recovers archetypes#✓fully proved

SPA recovers archetypes (Gillis–Vavasis Theorem 1, noiseless case): in the first r picks of any SPA run on a separable matrix with r archetypes, the picked columns are pairwise distinct.

theorem IsSPARun.map_nodup {m : ι → E} {r : ℕ} (hm : Separable m r) {S : List ι}
    (hS : IsSPARun m S) (hlen : S.length ≤ r) : (S.map m).Nodup

Uses 4 · Used by 1

Statement usesRun of the successive projection algorithm · Separable data matrix

Proof usesNorm bound for a sub-convex combination of vectors · Residual of a column in the successive projection algorithm

Used bySuccessive projection finds every archetype after r picks

TheoremSPA recovers archetypes#✓fully proved

SPA recovers archetypes (Gillis–Vavasis Theorem 1, noiseless case): each of the first r picks of any SPA run is an archetype.

theorem IsSPARun.mem_range {m : ι → E} {r : ℕ} (hm : Separable m r) {S : List ι}
    (hS : IsSPARun m S) (hlen : S.length ≤ r) : ∀ j ∈ S, m j ∈ Set.range hm.w

Uses 4 · Used by 1

Statement usesRun of the successive projection algorithm · Separable data matrix

Proof usesNorm bound for a sub-convex combination of vectors · Residual of a column in the successive projection algorithm

Used bySuccessive projection finds every archetype after r picks

TheoremSuccessive projection finds every archetype after r picks#✓fully proved

After exactly r picks, SPA has found every archetype.

theorem IsSPARun.range_eq {m : ι → E} {r : ℕ} (hm : Separable m r) {S : List ι}
    (hS : IsSPARun m S) (hlen : S.length = r) : {e | ∃ j ∈ S, m j = e} = Set.range hm.w

Uses 4

Statement usesRun of the successive projection algorithm · Separable data matrix

Proof usesSPA recovers archetypes · SPA recovers archetypes

TheoremExistence of successive projection runs of every length#✓fully proved

SPA runs of every length exist (on a nonempty set of columns).

theorem exists_isSPARun [Finite ι] [Nonempty ι] (m : ι → E) (n : ℕ) :
    ∃ S : List ι, S.length = n ∧ IsSPARun m S

Uses 2

Statement usesRun of the successive projection algorithm

Proof usesResidual of a column in the successive projection algorithm

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.