Non-negative matrix factorization

DefinitionObjective of nonnegative matrix factorization#✓fully proved

The NMF objective: the squared Frobenius distance ‖X - W H‖_F² = ∑ i j, (X i j - (W H) i j)² between the data X and the product W * H.

def objective [Fintype m] [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : ℝ :=
  ∑ i, ∑ j, (X i j - (W * H) i j) ^ 2

Used by 9

Used byExistence of a minimizer · Partial derivative of the NMF objective in an entry of H · Partial derivative of the NMF objective in an entry of W · Nonnegativity of the NMF objective · The objective is non-increasing along the Lee–Seung iterates · One Lee–Seung sweep does not increase the objective · The NMF objective is invariant under transposition · Lee–Seung, H step · Lee–Seung, W step

TheoremNonnegativity of the NMF objective#✓fully proved

The objective is nonnegative.

theorem objective_nonneg [Fintype m] [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) :
    0 ≤ objective X W H

Uses 1

Statement usesObjective of nonnegative matrix factorization

TheoremThe NMF objective is invariant under transposition#✓fully proved

Transposing exchanges the roles of W and H: ‖Xᵀ - Hᵀ Wᵀ‖² = ‖X - W H‖².

theorem objective_transpose [Fintype m] [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) :
    objective Xᵀ Hᵀ Wᵀ = objective X W H

Uses 1 · Used by 2

Statement usesObjective of nonnegative matrix factorization

Used byPartial derivative of the NMF objective in an entry of W · Lee–Seung, W step

TheoremExistence of a minimizer#✓fully proved

For every real matrix X and every finite inner index type k, the objective attains its infimum over pairs W, H ≥ 0 (entrywise).

theorem exists_minimizer [Fintype m] [Fintype n] [Fintype k] (X : Matrix m n ℝ) :
    ∃ W : Matrix m k ℝ, ∃ H : Matrix k n ℝ, (∀ i a, 0 ≤ W i a) ∧ (∀ a j, 0 ≤ H a j) ∧
      ∀ (W' : Matrix m k ℝ) (H' : Matrix k n ℝ), (∀ i a, 0 ≤ W' i a) → (∀ a j, 0 ≤ H' a j) →
        objective X W H ≤ objective X W' H'

Uses 1

Statement usesObjective of nonnegative matrix factorization

34 fully proved

Lee–Seung multiplicative updates

DefinitionLee–Seung multiplicative update of H#✓fully proved

The Lee–Seung multiplicative update of H (Lee and Seung 2001, Theorem 1): H a j ← H a j * (Wᵀ X) a j / (Wᵀ W H) a j. An entry with a zero denominator becomes 0 (Lean's x / 0 = 0).

noncomputable def updateH [Fintype m] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : Matrix k n ℝ :=
  Matrix.of fun a j => H a j * (Wᵀ * X) a j / (Wᵀ * W * H) a j

Used by 9

Used byPositive fixed points are KKT points · Complementary slackness at a fixed point of the H update · One Lee–Seung sweep does not increase the objective · Lee–Seung, H step · Lee–Seung, W step · One sweep of the Lee–Seung algorithm · A Lee–Seung sweep preserves nonnegativity · The Lee–Seung H update preserves nonnegativity · The W update is the H update of the transposed problem

DefinitionLee–Seung multiplicative update of W#✓fully proved

The Lee–Seung multiplicative update of W (Lee and Seung 2001, Theorem 1): W i a ← W i a * (X Hᵀ) i a / (W H Hᵀ) i a. An entry with a zero denominator becomes 0.

noncomputable def updateW [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : Matrix m k ℝ :=
  Matrix.of fun i a => W i a * (X * Hᵀ) i a / (W * H * Hᵀ) i a

Used by 7

Used byPositive fixed points are KKT points · Complementary slackness at a fixed point of the W update · One Lee–Seung sweep does not increase the objective · Lee–Seung, W step · One sweep of the Lee–Seung algorithm · The W update is the H update of the transposed problem · The Lee–Seung W update preserves nonnegativity

DefinitionOne sweep of the Lee–Seung algorithm#✓fully proved

One sweep of the Lee–Seung algorithm: update H, then update W using the new H.

noncomputable def sweep [Fintype m] [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (p : Matrix m k ℝ × Matrix k n ℝ) : Matrix m k ℝ × Matrix k n ℝ :=
  (updateW X p.1 (updateH X p.1 p.2), updateH X p.1 p.2)

Uses 2 · Used by 4

Statement usesLee–Seung multiplicative update of H · Lee–Seung multiplicative update of W

Used byPositive fixed points are KKT points · The objective is non-increasing along the Lee–Seung iterates · One Lee–Seung sweep does not increase the objective · A Lee–Seung sweep preserves nonnegativity

TheoremThe W update is the H update of the transposed problem#✓fully proved

The W update is the H update of the transposed problem.

theorem updateW_eq_transpose [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) :
    updateW X W H = (updateH Xᵀ Hᵀ Wᵀ)ᵀ

Uses 2 · Used by 1

Statement usesLee–Seung multiplicative update of H · Lee–Seung multiplicative update of W

Used byLee–Seung, W step

TheoremThe Lee–Seung H update preserves nonnegativity#✓fully proved

The H update keeps H nonnegative when X, W, H are nonnegative.

theorem updateH_nonneg [Fintype m] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ} {H : Matrix k n ℝ}
    (hX : ∀ i j, 0 ≤ X i j) (hW : ∀ i a, 0 ≤ W i a) (hH : ∀ a j, 0 ≤ H a j) (a : k) (j : n) :
    0 ≤ updateH X W H a j

Uses 1 · Used by 2

Statement usesLee–Seung multiplicative update of H

Used byOne Lee–Seung sweep does not increase the objective · A Lee–Seung sweep preserves nonnegativity

TheoremThe Lee–Seung W update preserves nonnegativity#✓fully proved

The W update keeps W nonnegative when X, W, H are nonnegative.

theorem updateW_nonneg [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ} {H : Matrix k n ℝ}
    (hX : ∀ i j, 0 ≤ X i j) (hW : ∀ i a, 0 ≤ W i a) (hH : ∀ a j, 0 ≤ H a j) (i : m) (a : k) :
    0 ≤ updateW X W H i a

Uses 1 · Used by 1

Statement usesLee–Seung multiplicative update of W

Used byA Lee–Seung sweep preserves nonnegativity

TheoremLee–Seung, H step#✓fully proved

Lee–Seung, H step (Lee and Seung 2001, Theorem 1): for W, H ≥ 0, the multiplicative update of H does not increase ‖X - W H‖_F². The proof is the auxiliary-function argument: the quadratic term of the exact expansion is bounded by Lee and Seung's diagonal majorant (here through a weighted Cauchy–Schwarz inequality), and the update minimizes the majorant. X may have any sign.

theorem objective_updateH_le [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ} {H : Matrix k n ℝ}
    (hW : ∀ i a, 0 ≤ W i a) (hH : ∀ a j, 0 ≤ H a j) :
    objective X W (updateH X W H) ≤ objective X W H

Uses 2 · Used by 2

Statement usesObjective of nonnegative matrix factorization · Lee–Seung multiplicative update of H

Used byOne Lee–Seung sweep does not increase the objective · Lee–Seung, W step

TheoremLee–Seung, W step#✓fully proved

For W, H ≥ 0, the multiplicative update of W does not increase ‖X - W H‖_F².

theorem objective_updateW_le [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ} {H : Matrix k n ℝ}
    (hW : ∀ i a, 0 ≤ W i a) (hH : ∀ a j, 0 ≤ H a j) :
    objective X (updateW X W H) H ≤ objective X W H

Uses 6 · Used by 1

Statement usesObjective of nonnegative matrix factorization · Lee–Seung multiplicative update of W

Proof usesThe NMF objective is invariant under transposition · Lee–Seung, H step · Lee–Seung multiplicative update of H · The W update is the H update of the transposed problem

Used byOne Lee–Seung sweep does not increase the objective

TheoremA Lee–Seung sweep preserves nonnegativity#✓fully proved

One sweep keeps both factors nonnegative when X ≥ 0.

theorem sweep_nonneg [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {p : Matrix m k ℝ × Matrix k n ℝ}
    (hX : ∀ i j, 0 ≤ X i j) (hW : ∀ i a, 0 ≤ p.1 i a) (hH : ∀ a j, 0 ≤ p.2 a j) :
    (∀ i a, 0 ≤ (sweep X p).1 i a) ∧ ∀ a j, 0 ≤ (sweep X p).2 a j

Uses 4 · Used by 1

Statement usesOne sweep of the Lee–Seung algorithm

Proof usesLee–Seung multiplicative update of H · The Lee–Seung H update preserves nonnegativity · The Lee–Seung W update preserves nonnegativity

Used byThe objective is non-increasing along the Lee–Seung iterates

TheoremOne Lee–Seung sweep does not increase the objective#✓fully proved

One Lee–Seung sweep does not increase the objective, for X, W, H ≥ 0.

theorem objective_sweep_le [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {p : Matrix m k ℝ × Matrix k n ℝ}
    (hX : ∀ i j, 0 ≤ X i j) (hW : ∀ i a, 0 ≤ p.1 i a) (hH : ∀ a j, 0 ≤ p.2 a j) :
    objective X (sweep X p).1 (sweep X p).2 ≤ objective X p.1 p.2

Uses 7 · Used by 1

Statement usesObjective of nonnegative matrix factorization · One sweep of the Lee–Seung algorithm

Proof usesLee–Seung, H step · Lee–Seung, W step · Lee–Seung multiplicative update of H · The Lee–Seung H update preserves nonnegativity · Lee–Seung multiplicative update of W

Used byThe objective is non-increasing along the Lee–Seung iterates

TheoremThe objective is non-increasing along the Lee–Seung iterates#✓fully proved

The objective is non-increasing along the Lee–Seung iterates started from W, H ≥ 0, for X ≥ 0.

theorem objective_sweep_iterate_antitone [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {p : Matrix m k ℝ × Matrix k n ℝ}
    (hX : ∀ i j, 0 ≤ X i j) (hW : ∀ i a, 0 ≤ p.1 i a) (hH : ∀ a j, 0 ≤ p.2 a j) :
    Antitone fun t : ℕ => objective X ((sweep X)^[t] p).1 ((sweep X)^[t] p).2

Uses 4

Statement usesObjective of nonnegative matrix factorization · One sweep of the Lee–Seung algorithm

Proof usesOne Lee–Seung sweep does not increase the objective · A Lee–Seung sweep preserves nonnegativity

Stationarity at fixed points

DefinitionGradient of the NMF objective with respect to H#✓fully proved

The gradient of the objective with respect to H: 2 (Wᵀ W H - Wᵀ X).

def gradH [Fintype m] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : Matrix k n ℝ :=
  (2 : ℝ) • (Wᵀ * W * H - Wᵀ * X)

Used by 5

Used byPartial derivative of the NMF objective in an entry of H · Partial derivative of the NMF objective in an entry of W · Karush–Kuhn–Tucker point of nonnegative matrix factorization · Positive fixed points are KKT points · Complementary slackness at a fixed point of the H update

DefinitionGradient of the NMF objective with respect to W#✓fully proved

The gradient of the objective with respect to W: 2 (W H Hᵀ - X Hᵀ).

def gradW [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : Matrix m k ℝ :=
  (2 : ℝ) • (W * H * Hᵀ - X * Hᵀ)

Used by 4

Used byPartial derivative of the NMF objective in an entry of W · Karush–Kuhn–Tucker point of nonnegative matrix factorization · Positive fixed points are KKT points · Complementary slackness at a fixed point of the W update

TheoremPartial derivative of the NMF objective in an entry of H#✓fully proved

gradH X W H a j is the partial derivative of the objective in the entry H a j.

theorem hasDerivAt_objective_H [Fintype m] [Fintype n] [Fintype k] [DecidableEq k] [DecidableEq n]
    (X : Matrix m n ℝ)
    (W : Matrix m k ℝ) (H : Matrix k n ℝ) (a : k) (j : n) :
    HasDerivAt (fun t : ℝ => objective X W (H + Matrix.single a j t)) (gradH X W H a j) 0

Uses 2 · Used by 1

Statement usesGradient of the NMF objective with respect to H · Objective of nonnegative matrix factorization

Used byPartial derivative of the NMF objective in an entry of W

TheoremPartial derivative of the NMF objective in an entry of W#✓fully proved

gradW X W H i a is the partial derivative of the objective in the entry W i a.

theorem hasDerivAt_objective_W [Fintype m] [Fintype n] [Fintype k] [DecidableEq m] [DecidableEq k]
    (X : Matrix m n ℝ)
    (W : Matrix m k ℝ) (H : Matrix k n ℝ) (i : m) (a : k) :
    HasDerivAt (fun t : ℝ => objective X (W + Matrix.single i a t) H) (gradW X W H i a) 0

Uses 5

Statement usesGradient of the NMF objective with respect to W · Objective of nonnegative matrix factorization

Proof usesGradient of the NMF objective with respect to H · Partial derivative of the NMF objective in an entry of H · The NMF objective is invariant under transposition

TheoremComplementary slackness at a fixed point of the H update#✓fully proved

If updateH X W H = H, then H a j * gradH X W H a j = 0 for every entry.

theorem mul_gradH_eq_zero_of_updateH_eq [Fintype m] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ}
    {H : Matrix k n ℝ} (hfix : updateH X W H = H) (a : k) (j : n) :
    H a j * gradH X W H a j = 0

Uses 2 · Used by 1

Statement usesGradient of the NMF objective with respect to H · Lee–Seung multiplicative update of H

Used byPositive fixed points are KKT points

TheoremComplementary slackness at a fixed point of the W update#✓fully proved

Complementary slackness at a fixed point of the W update.

theorem mul_gradW_eq_zero_of_updateW_eq [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ}
    {H : Matrix k n ℝ} (hfix : updateW X W H = W) (i : m) (a : k) :
    W i a * gradW X W H i a = 0

Uses 2 · Used by 1

Statement usesGradient of the NMF objective with respect to W · Lee–Seung multiplicative update of W

Used byPositive fixed points are KKT points

StructureKarush–Kuhn–Tucker point of nonnegative matrix factorization#✓fully proved

The Karush–Kuhn–Tucker conditions of min ‖X - W H‖_F² subject to W, H ≥ 0: primal feasibility, dual feasibility (nonnegative gradients) and complementary slackness.

structure IsKKTPoint [Fintype m] [Fintype n] [Fintype k]
    (X : Matrix m n ℝ) (W : Matrix m k ℝ) (H : Matrix k n ℝ) : Prop where
  /-- `W` is nonnegative. -/
  W_nonneg : ∀ i a, 0 ≤ W i a
  /-- `H` is nonnegative. -/
  H_nonneg : ∀ a j, 0 ≤ H a j
  /-- The gradient in `W` is nonnegative. -/
  gradW_nonneg : ∀ i a, 0 ≤ gradW X W H i a
  /-- The gradient in `H` is nonnegative. -/
  gradH_nonneg : ∀ a j, 0 ≤ gradH X W H a j
  /-- Complementary slackness in `W`. -/
  W_mul_gradW : ∀ i a, W i a * gradW X W H i a = 0
  /-- Complementary slackness in `H`. -/
  H_mul_gradH : ∀ a j, H a j * gradH X W H a j = 0

Uses 2 · Used by 1

Statement usesGradient of the NMF objective with respect to H · Gradient of the NMF objective with respect to W

Used byPositive fixed points are KKT points

TheoremPositive fixed points are KKT points#✓fully proved

A fixed point of the Lee–Seung sweep with all entries of W and H positive has both gradients zero, so it satisfies the KKT conditions.

theorem isKKTPoint_of_sweep_eq [Fintype m] [Fintype n] [Fintype k]
    {X : Matrix m n ℝ} {W : Matrix m k ℝ} {H : Matrix k n ℝ}
    (hfix : sweep X (W, H) = (W, H)) (hW : ∀ i a, 0 < W i a) (hH : ∀ a j, 0 < H a j) :
    IsKKTPoint X W H ∧ gradW X W H = 0 ∧ gradH X W H = 0

Uses 8

Statement usesKarush–Kuhn–Tucker point of nonnegative matrix factorization · Gradient of the NMF objective with respect to H · Gradient of the NMF objective with respect to W · One sweep of the Lee–Seung algorithm

Proof usesComplementary slackness at a fixed point of the H update · Complementary slackness at a fixed point of the W update · Lee–Seung multiplicative update of H · Lee–Seung multiplicative update of W

Identifiability under separability

DefinitionSeparable factor matrix#✓fully proved

H is separable: every factor a has a pure column, a column j of H equal to a positive multiple of the unit vector e_a. For X = W * H this makes column j of X a positive multiple of column a of W (a sample containing only factor a). Applied to Wᵀ it says that every factor has a pure row of W (an "anchor" feature of factor a alone).

def IsSeparable [DecidableEq k] (H : Matrix k n ℝ) : Prop :=
  ∀ a, ∃ j, ∃ c : ℝ, 0 < c ∧ ∀ b, H b j = if b = a then c else 0

Used by 1

Used byEssential uniqueness of NMF when both factors are separable

TheoremA nonnegative matrix with a nonnegative inverse is monomial#✓fully proved

If G * K = 1 with G and K entrywise nonnegative, then there are a permutation σ and positive weights d with G a b = d b if a = σ b and 0 otherwise.

theorem exists_perm_of_mul_eq_one [Fintype k] [DecidableEq k] {G K : Matrix k k ℝ}
    (hG : ∀ a b, 0 ≤ G a b) (hK : ∀ a b, 0 ≤ K a b) (hGK : G * K = 1) :
    ∃ σ : k ≃ k, ∃ d : k → ℝ, (∀ b, 0 < d b) ∧ ∀ a b, G a b = if a = σ b then d b else 0

Used by 1

Used byEssential uniqueness of NMF when both factors are separable

TheoremEssential uniqueness of NMF when both factors are separable#✓fully proved

Suppose X = W * H, where W has a pure row for every factor (IsSeparable Wᵀ: for each a a row i with W i · = e • e_a, e > 0) and H has a pure column for every factor (IsSeparable H). Then every factorization X = W' * H' with W', H' ≥ 0 and the same inner dimension agrees with (W, H) up to a permutation σ and positive scalings d of the factors: W' · a = d a • W · (σ a) and H' a · = (d a)⁻¹ • H (σ a) ·. The signs of W and H are not used. Proof: the anchor rows and columns of X form a positive diagonal block, so the matching block of W' is a nonnegative matrix with a nonnegative inverse, hence monomial (exists_perm_of_mul_eq_one).

theorem eq_of_isSeparable [Fintype k] [DecidableEq k] {X : Matrix m n ℝ}
    {W W' : Matrix m k ℝ} {H H' : Matrix k n ℝ} (hX : X = W * H) (hX' : X = W' * H')
    (hW' : ∀ i a, 0 ≤ W' i a) (hH' : ∀ a j, 0 ≤ H' a j) (hsW : IsSeparable Wᵀ)
    (hsH : IsSeparable H) :
    ∃ σ : k ≃ k, ∃ d : k → ℝ, (∀ a, 0 < d a) ∧ (∀ i a, W' i a = d a * W i (σ a)) ∧
      ∀ a j, H' a j = (d a)⁻¹ * H (σ a) j

Uses 2

Statement usesSeparable factor matrix

Proof usesA nonnegative matrix with a nonnegative inverse is monomial

Nonnegative rank

DefinitionNonnegative rank of a matrix#✓fully proved

The nonnegative rank of X: the least r such that X = W * H with W : m × r and H : r × n entrywise nonnegative (Cohen and Rothblum 1993). If X has a negative entry no such factorization exists and the value is the junk value sInf ∅ = 0.

noncomputable def nonnegRank (X : Matrix m n ℝ) : ℕ :=
  sInf {r | ∃ (W : Matrix m (Fin r) ℝ) (H : Matrix (Fin r) n ℝ),
    (∀ i a, 0 ≤ W i a) ∧ (∀ a j, 0 ≤ H a j) ∧ W * H = X}

Used by 4

Used byExistence of a factorization of nonnegative-rank inner dimension · Nonnegative rank is at most the number of columns · A nonnegative factorization bounds the nonnegative rank · The nonnegative rank of a nonnegative matrix is at least its rank

TheoremA nonnegative factorization bounds the nonnegative rank#✓fully proved

A nonnegative factorization with inner dimension r bounds the nonnegative rank by r.

theorem nonnegRank_le_of_mul_eq {r : ℕ} {X : Matrix m n ℝ} (W : Matrix m (Fin r) ℝ)
    (H : Matrix (Fin r) n ℝ) (hW : ∀ i a, 0 ≤ W i a) (hH : ∀ a j, 0 ≤ H a j) (hX : W * H = X) :
    nonnegRank X ≤ r

Uses 1 · Used by 1

Statement usesNonnegative rank of a matrix

Used byNonnegative rank is at most the number of columns

TheoremExistence of a factorization of nonnegative-rank inner dimension#✓fully proved

A nonnegative matrix has a nonnegative factorization of inner dimension nonnegRank X.

theorem exists_mul_eq_nonnegRank [Finite n] {X : Matrix m n ℝ} (hX : ∀ i j, 0 ≤ X i j) :
    ∃ (W : Matrix m (Fin (nonnegRank X)) ℝ) (H : Matrix (Fin (nonnegRank X)) n ℝ),
      (∀ i a, 0 ≤ W i a) ∧ (∀ a j, 0 ≤ H a j) ∧ W * H = X

Uses 1 · Used by 1

Statement usesNonnegative rank of a matrix

Used byThe nonnegative rank of a nonnegative matrix is at least its rank

TheoremNonnegative rank is at most the number of columns#✓fully proved

The nonnegative rank of a nonnegative matrix is at most its number of columns.

theorem nonnegRank_le_card_width [Fintype n] {X : Matrix m n ℝ} (hX : ∀ i j, 0 ≤ X i j) :
    nonnegRank X ≤ Fintype.card n

Uses 2

Statement usesNonnegative rank of a matrix

Proof usesA nonnegative factorization bounds the nonnegative rank

TheoremThe nonnegative rank of a nonnegative matrix is at least its rank#✓fully proved

The nonnegative rank of a nonnegative matrix is at least its rank.

theorem rank_le_nonnegRank [Fintype n] {X : Matrix m n ℝ} (hX : ∀ i j, 0 ≤ X i j) :
    X.rank ≤ nonnegRank X

Uses 2

Statement usesNonnegative rank of a matrix

Proof usesExistence of a factorization of nonnegative-rank inner dimension

Applications

TheoremColumn sums of a matrix product#✓fully proved

Column sums of a product: ∑ i, (W H) i j = ∑ a, (∑ i, W i a) H a j.

theorem sum_mul_apply [Fintype m] [Fintype k] (W : Matrix m k ℝ) (H : Matrix k n ℝ) (j : n) :
    ∑ i, (W * H) i j = ∑ a, (∑ i, W i a) * H a j

Used by 1

Used byMutational signatures

TheoremMutational signatures#✓fully proved

Mutational signatures (Alexandrov et al. 2013). Write the mutation-count matrix (mutation types × samples) as W * H, signatures (columns of W) times exposures H. If every signature is a probability vector over mutation types, the total mutation count of sample j equals the sum of its exposures.

theorem sum_mul_apply_of_sum_eq_one [Fintype m] [Fintype k]
    {W : Matrix m k ℝ} (hW : ∀ a, ∑ i, W i a = 1)
    (H : Matrix k n ℝ) (j : n) : ∑ i, (W * H) i j = ∑ a, H a j

Uses 1

Proof usesColumn sums of a matrix product

TheoremGene-expression deconvolution#✓fully proved

Write the bulk matrix (genes × samples) as C * P, the cell-type profiles C times the cell-type proportions P. If the proportions of sample j are nonnegative and sum to 1 and every cell type expresses gene g at a level in [lo, hi], then the bulk level of g in sample j lies in [lo, hi].

theorem mul_apply_mem_Icc [Fintype k]
    {C : Matrix m k ℝ} {P : Matrix k n ℝ} {g : m} {j : n} {lo hi : ℝ}
    (hP : ∀ a, 0 ≤ P a j) (hsum : ∑ a, P a j = 1) (hC : ∀ a, C g a ∈ Set.Icc lo hi) :
    (C * P) g j ∈ Set.Icc lo hi

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.