GPS model of ChIP-seq binding events

DefinitionSurviving weight of a GPS event#✓fully proved

The surviving weight max (N j - α) 0 of event j, for expected read counts N and sparseness parameter α.

noncomputable def survivorWeight (α : ℝ) (N : ι → ℝ) (j : ι) : ℝ := max (N j - α) 0

Used by 11

Used byThe GPS M-step with component elimination · Elimination · Nonnegativity of the GPS M-step update · GPS M-step formula when every event survives · GPS M-step at zero sparseness is the ordinary mixture M-step · GPS M-step update sums to one when some event survives · Total surviving weight is positive iff some event survives · Nonnegativity of surviving weights · Truncated GPS objective · Truncated and penalized objectives agree when every event survives · The update is an upper bound for the truncated objective

DefinitionThe GPS M-step with component elimination#✓fully proved

π j = max (N j - α) 0 / ∑ k, max (N k - α) 0.

noncomputable def mStep [Fintype ι] (α : ℝ) (N : ι → ℝ) (j : ι) : ℝ :=
  survivorWeight α N j / ∑ k, survivorWeight α N k

Uses 1 · Used by 8

Statement usesSurviving weight of a GPS event

Used byElimination · Nonnegativity of the GPS M-step update · GPS M-step formula when every event survives · GPS M-step keeps positive probability exactly on surviving events · GPS M-step at zero sparseness is the ordinary mixture M-step · The M-step of the restructured model · GPS M-step update sums to one when some event survives · The update is an upper bound for the truncated objective

DefinitionExpected penalized complete-data log-likelihood of GPS#✓fully proved

The expected complete-data log penalized likelihood of GPS, up to an additive constant: ∑ j, (N j - α) log (π j) (the expected log-likelihood ∑ j, N j log (π j) plus the log of the negative Dirichlet prior). Meaningful for positive π.

noncomputable def penalizedQ [Fintype ι] (α : ℝ) (N π : ι → ℝ) : ℝ := ∑ j, (N j - α) * log (π j)

Used by 2

Used byThe M-step of the restructured model · Truncated and penalized objectives agree when every event survives

DefinitionTruncated GPS objective#✓fully proved

The truncated objective ∑ j, max (N j - α) 0 * log (π j).

noncomputable def truncatedQ [Fintype ι] (α : ℝ) (N π : ι → ℝ) : ℝ :=
  ∑ j, survivorWeight α N j * log (π j)

Uses 1 · Used by 3

Statement usesSurviving weight of a GPS event

Used byThe M-step of the restructured model · Truncated and penalized objectives agree when every event survives · The update is an upper bound for the truncated objective

TheoremNonnegativity of surviving weights#✓fully proved

Surviving weights are nonnegative.

theorem survivorWeight_nonneg (α : ℝ) (N : ι → ℝ) (j : ι) : 0 ≤ survivorWeight α N j

Uses 1 · Used by 3

Statement usesSurviving weight of a GPS event

Used byNonnegativity of the GPS M-step update · Total surviving weight is positive iff some event survives · The update is an upper bound for the truncated objective

TheoremTotal surviving weight is positive iff some event survives#✓fully proved

The total surviving weight is positive iff some event has α < N j.

theorem sum_survivorWeight_pos {α : ℝ} {N : ι → ℝ} {j₀ : ι} (h : α < N j₀) :
    0 < ∑ k, survivorWeight α N k

Uses 2 · Used by 3

Statement usesSurviving weight of a GPS event

Proof usesNonnegativity of surviving weights

Used byElimination · GPS M-step update sums to one when some event survives · The update is an upper bound for the truncated objective

TheoremNonnegativity of the GPS M-step update#✓fully proved

The update is nonnegative.

theorem mStep_nonneg (α : ℝ) (N : ι → ℝ) (j : ι) : 0 ≤ mStep α N j

Uses 3 · Used by 1

Statement usesThe GPS M-step with component elimination

Proof usesSurviving weight of a GPS event · Nonnegativity of surviving weights

Used byGPS M-step keeps positive probability exactly on surviving events

TheoremGPS M-step update sums to one when some event survives#✓fully proved

The update sums to one when some event survives.

theorem sum_mStep {α : ℝ} {N : ι → ℝ} {j₀ : ι} (h : α < N j₀) : ∑ j, mStep α N j = 1

Uses 3

Statement usesThe GPS M-step with component elimination

Proof usesTotal surviving weight is positive iff some event survives · Surviving weight of a GPS event

TheoremElimination#✓fully proved

When some event survives, event j gets probability zero iff N j ≤ α.

theorem mStep_eq_zero_iff {α : ℝ} {N : ι → ℝ} {j₀ : ι} (h : α < N j₀) (j : ι) :
    mStep α N j = 0 ↔ N j ≤ α

Uses 3 · Used by 1

Statement usesThe GPS M-step with component elimination

Proof usesTotal surviving weight is positive iff some event survives · Surviving weight of a GPS event

Used byGPS M-step keeps positive probability exactly on surviving events

TheoremGPS M-step keeps positive probability exactly on surviving events#✓fully proved

When some event survives, event j keeps positive probability iff α < N j.

theorem mStep_pos_iff {α : ℝ} {N : ι → ℝ} {j₀ : ι} (h : α < N j₀) (j : ι) :
    0 < mStep α N j ↔ α < N j

Uses 3

Statement usesThe GPS M-step with component elimination

Proof usesElimination · Nonnegativity of the GPS M-step update

TheoremGPS M-step at zero sparseness is the ordinary mixture M-step#✓fully proved

With α = 0 and nonnegative counts the update is the ordinary mixture M-step N j / ∑ N.

theorem mStep_zero {N : ι → ℝ} (hN : ∀ j, 0 ≤ N j) (j : ι) :
    mStep 0 N j = N j / ∑ k, N k

Uses 2

Statement usesThe GPS M-step with component elimination

Proof usesSurviving weight of a GPS event

TheoremThe update is an upper bound for the truncated objective#✓fully proved

The update is an upper bound for the truncated objective over the positive probability vectors (derived characterization of the elimination rule). Upper-bound statement only: this does not prove the value at mStep is the supremum (no approximation or sSup theorem is given). When elimination occurs mStep itself is not a positive vector (eliminated coordinates are zero), so it is the boundary point on the face where eliminated coordinates vanish, not a maximizer inside the positive simplex.

theorem truncatedQ_le_mStep {α : ℝ} {N : ι → ℝ} {j₀ : ι} (h : α < N j₀) {π : ι → ℝ}
    (hπ : ∀ j, 0 < π j) (hsum : ∑ j, π j = 1) :
    truncatedQ α N π ≤ truncatedQ α N (mStep α N)

Uses 6 · Used by 1

Statement usesThe GPS M-step with component elimination · Truncated GPS objective

Proof usesTotal surviving weight is positive iff some event survives · Surviving weight of a GPS event · Nonnegativity of surviving weights · The weighted log-likelihood is bounded by its value at the normalized counts

Used byThe M-step of the restructured model

TheoremTruncated and penalized objectives agree when every event survives#✓fully proved

When every event survives, the penalized and truncated objectives agree.

theorem truncatedQ_eq_penalizedQ {α : ℝ} {N : ι → ℝ} (h : ∀ j, α < N j) (π : ι → ℝ) :
    truncatedQ α N π = penalizedQ α N π

Uses 3 · Used by 1

Statement usesExpected penalized complete-data log-likelihood of GPS · Truncated GPS objective

Proof usesSurviving weight of a GPS event

Used byThe M-step of the restructured model

TheoremGPS M-step formula when every event survives#✓fully proved

When every event survives, the update is (N j - α) / ∑ k, (N k - α).

theorem mStep_of_forall_lt {α : ℝ} {N : ι → ℝ} (h : ∀ j, α < N j) (j : ι) :
    mStep α N j = (N j - α) / ∑ k, (N k - α)

Uses 2

Statement usesThe GPS M-step with component elimination

Proof usesSurviving weight of a GPS event

TheoremThe M-step of the restructured model#✓fully proved

When every remaining event survives (α < N j for all j), the update maximizes the GPS expected complete-data log penalized likelihood over the positive probability vectors.

theorem penalizedQ_le_mStep [Nonempty ι] {α : ℝ} {N : ι → ℝ} (h : ∀ j, α < N j) {π : ι → ℝ}
    (hπ : ∀ j, 0 < π j) (hsum : ∑ j, π j = 1) :
    penalizedQ α N π ≤ penalizedQ α N (mStep α N)

Uses 5

Statement usesThe GPS M-step with component elimination · Expected penalized complete-data log-likelihood of GPS

Proof usesTruncated GPS objective · Truncated and penalized objectives agree when every event survives · The update is an upper bound for the truncated objective

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.