Archetypal analysis

DefinitionResidual sum of squares in archetypal analysis#✓fully proved

The residual sum of squares of archetypes z for the data x: each data point is replaced by the closest point of the convex hull of the archetypes. This is only meaningful for 0 < p: for p = 0 the hull is empty and infDist to the empty set is 0 by convention, so rss is 0 vacuously and must not be read as a perfect fit.

noncomputable def rss (x : Fin n → E) (z : Fin p → E) : ℝ :=
  ∑ i, infDist (x i) (convexHull ℝ (range z)) ^ 2

Used by 4

Used byExistence of an archetype minimizer on the hull boundary · Feasible archetypes can be moved to the boundary of the hull · The sample mean is the optimal single archetype · The RSS vanishes when the archetypes' convex hull contains the data

DefinitionFeasible archetypes#✓fully proved

Archetypes are feasible if each is a mixture of the data points.

def Feasible (x : Fin n → E) (z : Fin p → E) : Prop :=
  ∀ k, z k ∈ convexHull ℝ (range x)

Used by 3

Used byExistence of an archetype minimizer on the hull boundary · Feasible archetypes can be moved to the boundary of the hull · The sample mean is the optimal single archetype

DefinitionSample mean of the data#✓fully proved

The sample mean of the data.

noncomputable def mean (x : Fin n → E) : E := (n : ℝ)⁻¹ • ∑ i, x i

Used by 1

Used byThe sample mean is the optimal single archetype

TheoremThe sample mean is the optimal single archetype#✓fully proved

Cutler–Breiman Proposition 1(i): with a single archetype, the sample mean is feasible and minimizes the RSS.

theorem rss_const_mean_le (x : Fin n → E) (hn : 0 < n) (z : Fin 1 → E) :
    Feasible x (fun _ : Fin 1 => mean x) ∧ rss x (fun _ : Fin 1 => mean x) ≤ rss x z

Uses 3

Statement usesFeasible archetypes · Sample mean of the data · Residual sum of squares in archetypal analysis

TheoremFeasible archetypes can be moved to the boundary of the hull#✓fully proved

Cutler–Breiman Proposition 1(ii): for at least two archetypes, any feasible archetypes can be replaced by feasible archetypes on the boundary of the convex hull of the data whose convex hull contains the original one; in particular the RSS does not increase.

theorem exists_frontier_rss_le [Nontrivial E] (x : Fin n → E) (hp : 2 ≤ p) (z : Fin p → E)
    (hz : Feasible x z) :
    ∃ z' : Fin p → E, Feasible x z' ∧ (∀ k, z' k ∈ frontier (convexHull ℝ (range x))) ∧
      convexHull ℝ (range z) ⊆ convexHull ℝ (range z') ∧ rss x z' ≤ rss x z

Uses 2 · Used by 1

Statement usesFeasible archetypes · Residual sum of squares in archetypal analysis

Used byExistence of an archetype minimizer on the hull boundary

TheoremExistence of an archetype minimizer on the hull boundary#✓fully proved

If the RSS has a feasible minimizer with p ≥ 2 archetypes, it has one with every archetype on the boundary of the convex hull of the data.

theorem exists_frontier_minimizer [Nontrivial E] (x : Fin n → E) (hp : 2 ≤ p) (z : Fin p → E)
    (hz : Feasible x z) (hmin : ∀ z' : Fin p → E, Feasible x z' → rss x z ≤ rss x z') :
    ∃ z' : Fin p → E, Feasible x z' ∧ (∀ k, z' k ∈ frontier (convexHull ℝ (range x))) ∧
      ∀ z'' : Fin p → E, Feasible x z'' → rss x z' ≤ rss x z''

Uses 3

Statement usesFeasible archetypes · Residual sum of squares in archetypal analysis

Proof usesFeasible archetypes can be moved to the boundary of the hull

TheoremThe RSS vanishes when the archetypes' convex hull contains the data#✓fully proved

Cutler–Breiman Proposition 1(iii): if every data point is a mixture of the archetypes, the RSS vanishes. Requires 0 < p: for p = 0 the hull is empty, so rss is 0 vacuously and the vanishing would not witness a fit.

theorem rss_eq_zero_of_subset (x : Fin n → E) (z : Fin p → E) (hp : 0 < p)
    (h : ∀ i, x i ∈ convexHull ℝ (range z)) : rss x z = 0

Uses 1

Statement usesResidual sum of squares in archetypal analysis

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.