Mutational signatures and Bayesian NMF

DefinitionGeneralized Kullback–Leibler divergence#✓fully proved

The Kullback–Leibler β = 1 divergence d(x | y) = x log (x / y) - x + y (Tan–Févotte, Eq. 4). With Mathlib's 0 * log _ = 0 it gives d(0 | y) = y, the correct value; y > 0 is needed when x > 0.

noncomputable def klDiv (x y : ℝ) : ℝ := x * Real.log (x / y) - x + y

Used by 3

Used byData-fit term of the ARD-NMF objective · The H update is monotone · The W update is monotone

DefinitionReconstruction matrix in nonnegative matrix factorization#✓fully proved

The reconstruction (W H)_fn = ∑_k w_fk h_kn.

def recon (W : F → K → ℝ) (H : K → N → ℝ) (f : F) (n : N) : ℝ := ∑ k, W f k * H k n

Used by 7

Used byData-fit term of the ARD-NMF objective · The H update is monotone · The W update is monotone · ARD multiplicative update of H · A pruned entry stays pruned · ARD multiplicative update of W · A pruned entry stays pruned

DefinitionData-fit term of the ARD-NMF objective#✓fully proved

The data-fit term D_1(V | W H) = ∑_{f,n} d(v_fn | (W H)_fn).

noncomputable def dataFit (V : F → N → ℝ) (W : F → K → ℝ) (H : K → N → ℝ) : ℝ :=
  ∑ f, ∑ n, klDiv (V f n) (recon W H f n)

Uses 2 · Used by 3

Statement usesGeneralized Kullback–Leibler divergence · Reconstruction matrix in nonnegative matrix factorization

Used byH-dependent part of the ARD-NMF objective · W-dependent part of the ARD-NMF objective · The W update is monotone

DefinitionH-dependent part of the ARD-NMF objective#✓fully proved

The H-dependent part D_1(V | W H) / φ + ∑_{k,n} h_kn / λ_k of the ℓ₁-ARD objective (Tan–Févotte, Eq. 20, β = 1).

noncomputable def objectiveH (φ : ℝ) (V : F → N → ℝ) (W : F → K → ℝ) (lam : K → ℝ)
    (H : K → N → ℝ) : ℝ :=
  dataFit V W H / φ + ∑ k, ∑ n, H k n / lam k

Uses 1 · Used by 2

Statement usesData-fit term of the ARD-NMF objective

Used byThe H update is monotone · The W update is monotone

DefinitionARD multiplicative update of H#✓fully proved

The ℓ₁-ARD multiplicative update of H for β = 1 (Tan–Févotte, Eq. 32, Algorithm 2): h_kn ← h_kn (∑_f w_fk v_fn / (W H)_fn) / (∑_f w_fk + φ / λ_k).

noncomputable def updateH (φ : ℝ) (V : F → N → ℝ) (W : F → K → ℝ) (lam : K → ℝ)
    (H : K → N → ℝ) (k : K) (n : N) : ℝ :=
  H k n * (∑ f, W f k * V f n / recon W H f n) / (∑ f, W f k + φ / lam k)

Uses 1 · Used by 3

Statement usesReconstruction matrix in nonnegative matrix factorization

Used byThe H update is monotone · The W update is monotone · A pruned entry stays pruned

TheoremThe H update is monotone#✓fully proved

The H update is monotone (Tan–Févotte 2013, §IV-B, β = 1): it does not increase D_1(V | W H) / φ + ∑ h_kn / λ_k, for φ > 0, λ > 0, V ≥ 0, W ≥ 0 with no zero row, and H > 0 entrywise.

theorem objectiveH_updateH_le {φ : ℝ} {V : F → N → ℝ} {W : F → K → ℝ} {lam : K → ℝ}
    {H : K → N → ℝ} (hφ : 0 < φ) (hlam : ∀ k, 0 < lam k) (hV : ∀ f n, 0 ≤ V f n)
    (hW : ∀ f k, 0 ≤ W f k) (hWrow : ∀ f, ∃ k, 0 < W f k) (hH : ∀ k n, 0 < H k n) :
    objectiveH φ V W lam (updateH φ V W lam H) ≤ objectiveH φ V W lam H

Uses 4 · Used by 1

Statement usesH-dependent part of the ARD-NMF objective · ARD multiplicative update of H

Proof usesGeneralized Kullback–Leibler divergence · Reconstruction matrix in nonnegative matrix factorization

Used byThe W update is monotone

DefinitionW-dependent part of the ARD-NMF objective#✓fully proved

The W-dependent part D_1(V | W H) / φ + ∑_{f,k} w_fk / λ_k of the ℓ₁-ARD objective (Tan–Févotte, Eq. 20, β = 1).

noncomputable def objectiveW (φ : ℝ) (V : F → N → ℝ) (H : K → N → ℝ) (lam : K → ℝ)
    (W : F → K → ℝ) : ℝ :=
  dataFit V W H / φ + ∑ k, ∑ f, W f k / lam k

Uses 1 · Used by 1

Statement usesData-fit term of the ARD-NMF objective

Used byThe W update is monotone

DefinitionARD multiplicative update of W#✓fully proved

The ℓ₁-ARD multiplicative update of W for β = 1 (Tan–Févotte, Algorithm 2): w_fk ← w_fk (∑_n v_fn h_kn / (W H)_fn) / (∑_n h_kn + φ / λ_k).

noncomputable def updateW (φ : ℝ) (V : F → N → ℝ) (H : K → N → ℝ) (lam : K → ℝ)
    (W : F → K → ℝ) (f : F) (k : K) : ℝ :=
  W f k * (∑ n, V f n * H k n / recon W H f n) / (∑ n, H k n + φ / lam k)

Uses 1 · Used by 2

Statement usesReconstruction matrix in nonnegative matrix factorization

Used byThe W update is monotone · A pruned entry stays pruned

TheoremThe W update is monotone#✓fully proved

It does not increase D_1(V | W H) / φ + ∑ w_fk / λ_k, for φ > 0, λ > 0, V ≥ 0, H ≥ 0 with no zero column, and W > 0 entrywise (the transpose of objectiveH_updateH_le).

theorem objectiveW_updateW_le {φ : ℝ} {V : F → N → ℝ} {H : K → N → ℝ} {lam : K → ℝ}
    {W : F → K → ℝ} (hφ : 0 < φ) (hlam : ∀ k, 0 < lam k) (hV : ∀ f n, 0 ≤ V f n)
    (hH : ∀ k n, 0 ≤ H k n) (hHcol : ∀ n, ∃ k, 0 < H k n) (hW : ∀ f k, 0 < W f k) :
    objectiveW φ V H lam (updateW φ V H lam W) ≤ objectiveW φ V H lam W

Uses 8

Statement usesW-dependent part of the ARD-NMF objective · ARD multiplicative update of W

Proof usesData-fit term of the ARD-NMF objective · Generalized Kullback–Leibler divergence · H-dependent part of the ARD-NMF objective · The H update is monotone · Reconstruction matrix in nonnegative matrix factorization · ARD multiplicative update of H

DefinitionRelevance update in ARD-NMF#✓fully proved

The relevance update λ_k = (‖w_k‖₁ + ‖h_k‖₁ + b) / c (Tan–Févotte, Eq. 33, ℓ₁ prior; c = F + N + a + 1).

noncomputable def relevance (W : F → K → ℝ) (H : K → N → ℝ) (b c : ℝ) (k : K) : ℝ :=
  (∑ f, W f k + ∑ n, H k n + b) / c

Used by 2

Used byLower bound on the relevance update · Pruning

TheoremThe relevance update is the exact minimizer#✓fully proved

The relevance update is the exact minimizer (Tan–Févotte, §IV-C): for A > 0 and c > 0, λ ↦ A / λ + c log λ attains its minimum over λ > 0 at λ = A / c.

theorem relevance_isMinOn {A c : ℝ} (hA : 0 < A) (hc : 0 < c) :
    IsMinOn (fun l => A / l + c * Real.log l) (Set.Ioi 0) (A / c)

TheoremThe minimizer is unique#✓fully proved

If λ > 0 does as well as A / c, then λ = A / c.

theorem relevance_unique {A c l : ℝ} (hA : 0 < A) (hc : 0 < c) (hl : 0 < l)
    (h : A / l + c * Real.log l ≤ A / (A / c) + c * Real.log (A / c)) : l = A / c

TheoremLower bound on the relevance update#✓fully proved

The relevance never falls below its floor b / c (W, H ≥ 0, c > 0).

theorem div_le_relevance {W : F → K → ℝ} {H : K → N → ℝ} {b c : ℝ} (hc : 0 < c)
    (hW : ∀ f k, 0 ≤ W f k) (hH : ∀ k n, 0 ≤ H k n) (k : K) :
    b / c ≤ relevance W H b c k

Uses 1

Statement usesRelevance update in ARD-NMF

TheoremPruning#✓fully proved

Pruning (Tan–Févotte, §IV-D): the relevance equals its floor b / c exactly when the k-th column of W and the k-th row of H are zero (W, H ≥ 0, c > 0).

theorem relevance_eq_floor_iff {W : F → K → ℝ} {H : K → N → ℝ} {b c : ℝ} (hc : 0 < c)
    (hW : ∀ f k, 0 ≤ W f k) (hH : ∀ k n, 0 ≤ H k n) (k : K) :
    relevance W H b c k = b / c ↔ (∀ f, W f k = 0) ∧ ∀ n, H k n = 0

Uses 1

Statement usesRelevance update in ARD-NMF

TheoremA pruned entry stays pruned#✓fully proved

The multiplicative update maps a zero entry of H to zero.

theorem updateH_eq_zero (φ : ℝ) (V : F → N → ℝ) (W : F → K → ℝ) (lam : K → ℝ)
    {H : K → N → ℝ} {k : K} {n : N} (h : H k n = 0) : updateH φ V W lam H k n = 0

Uses 2

Statement usesARD multiplicative update of H

Proof usesReconstruction matrix in nonnegative matrix factorization

TheoremA pruned entry stays pruned#✓fully proved

The multiplicative update maps a zero entry of W to zero.

theorem updateW_eq_zero (φ : ℝ) (V : F → N → ℝ) (H : K → N → ℝ) (lam : K → ℝ)
    {W : F → K → ℝ} {f : F} {k : K} (h : W f k = 0) : updateW φ V H lam W f k = 0

Uses 2

Statement usesARD multiplicative update of W

Proof usesReconstruction matrix in nonnegative matrix factorization

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.