Admixture model and the FRAPPE EM algorithm

40 fully proved

The model

StructureParameters of the admixture model#✓fully proved

Parameters θ = (Q, F) of the admixture model: positive ancestry proportions Q i k summing to one over k, and reference-allele frequencies F k j strictly between 0 and 1.

structure Params where
  /-- The ancestry proportion of population `k` in individual `i`. -/
  Q : I → K → ℝ
  /-- The reference-allele frequency of SNP `j` in population `k`. -/
  F : K → J → ℝ
  /-- Ancestry proportions are positive. -/
  Q_pos : ∀ i k, 0 < Q i k
  /-- Ancestry proportions of each individual sum to one. -/
  Q_sum : ∀ i, ∑ k, Q i k = 1
  /-- Allele frequencies are positive. -/
  F_pos : ∀ k j, 0 < F k j
  /-- Allele frequencies are below one. -/
  F_lt_one : ∀ k j, F k j < 1

Used by 34

Used byAdmixture log-likelihood · The admixture log-likelihood is monotone along the FRAPPE EM iterates · The admixture log-likelihood is monotone along the iterates · Each FRAPPE EM step does not decrease the admixture log-likelihood · The EM theorem for the admixture model · Expected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Expected ancestry count of an individual · Positivity of the expected ancestry counts · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · The FRAPPE EM step · Joint weight of an allele copy and its ancestral population · Positivity of the admixture joint weight · The EM log-likelihood of the allele copies is the admixture log-likelihood · FRAPPE update of the allele frequencies · Updated allele frequencies are less than one · Positivity of the updated allele frequencies · FRAPPE update of the ancestry proportions · Positivity of the updated ancestry proportions · Updated ancestry proportions sum to one · The marginal of an allele copy · Expected population count of a SNP · Positivity of expected population counts on polymorphic data · Reference-allele probability in the admixture model · Reference-allele probability is less than one · Positivity of the reference-allele probability · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data · Ancestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities · Expected ancestry counts sum to the number of allele copies · Admixture responsibilities sum to one

DefinitionReference-allele probability in the admixture model#✓fully proved

The reference-allele probability qf θ i j = ∑ k, Q i k * F k j of a copy of SNP j in individual i.

noncomputable def qf (θ : Params I J K) (i : I) (j : J) : ℝ := ∑ k, θ.Q i k * θ.F k j

Uses 1 · Used by 5

Statement usesParameters of the admixture model

Used byAdmixture log-likelihood · The EM log-likelihood of the allele copies is the admixture log-likelihood · The marginal of an allele copy · Reference-allele probability is less than one · Positivity of the reference-allele probability

DefinitionJoint weight of an allele copy and its ancestral population#✓fully proved

The joint weight of an allele copy (i, j, a) and its ancestral population k: Q i k * (if a then F k j else 1 - F k j).

noncomputable def joint (θ : Params I J K) (x : I × J × Bool) (k : K) : ℝ :=
  θ.Q x.1 k * if x.2.2 then θ.F k x.2.1 else 1 - θ.F k x.2.1

Uses 1 · Used by 11

Statement usesParameters of the admixture model

Used byThe admixture log-likelihood is monotone along the iterates · The EM theorem for the admixture model · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · Positivity of the admixture joint weight · The EM log-likelihood of the allele copies is the admixture log-likelihood · The marginal of an allele copy · Reference-allele probability is less than one · Ancestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities · Admixture responsibilities sum to one

TheoremPositivity of the admixture joint weight#✓fully proved

The joint weight is positive (the standing hypothesis of the generic EM).

theorem joint_pos (θ : Params I J K) (x : I × J × Bool) (k : K) : 0 < joint θ x k

Uses 2 · Used by 5

Statement usesParameters of the admixture model · Joint weight of an allele copy and its ancestral population

Used byThe admixture log-likelihood is monotone along the iterates · The EM theorem for the admixture model · Reference-allele probability is less than one · Positivity of the admixture responsibilities · Admixture responsibilities sum to one

TheoremThe marginal of an allele copy#✓fully proved

Reference with probability qf θ i j, alternative with probability 1 - qf θ i j.

theorem marginal_eq (θ : Params I J K) (i : I) (j : J) (a : Bool) :
    marginal joint θ (i, j, a) = if a then qf θ i j else 1 - qf θ i j

Uses 4 · Used by 2

Statement usesParameters of the admixture model · Joint weight of an allele copy and its ancestral population · Reference-allele probability in the admixture model · Marginal of a latent-variable model

Used byThe EM log-likelihood of the allele copies is the admixture log-likelihood · Reference-allele probability is less than one

TheoremPositivity of the reference-allele probability#✓fully proved

The reference-allele probability is positive.

theorem qf_pos [Nonempty K] (θ : Params I J K) (i : I) (j : J) : 0 < qf θ i j

Uses 2

Statement usesParameters of the admixture model · Reference-allele probability in the admixture model

TheoremReference-allele probability is less than one#✓fully proved

The reference-allele probability is below one.

theorem qf_lt_one [Nonempty K] (θ : Params I J K) (i : I) (j : J) : qf θ i j < 1

Uses 6

Statement usesParameters of the admixture model · Reference-allele probability in the admixture model

Proof usesJoint weight of an allele copy and its ancestral population · Positivity of the admixture joint weight · The marginal of an allele copy · Marginal of a latent-variable model

The data: two allele copies per genotype

DefinitionReference-allele indicator for a genotype copy#✓fully proved

Whether copy c of the genotype g i j (with g i j reference copies) carries the reference allele: copies c < g i j do.

def isRef (g : I → J → Fin 3) (i : I) (j : J) (c : Fin 2) : Bool := decide (c.val < (g i j).val)

Used by 7

Used byExpected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Observation of one allele copy of a genotype · Decomposition of the admixture EM objective · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data

DefinitionObservation of one allele copy of a genotype#✓fully proved

The observation (i, j, a) of copy c of genotype g i j.

def copyAllele (g : I → J → Fin 3) (x : I × J × Fin 2) : I × J × Bool :=
  (x.1, x.2.1, isRef g x.1 x.2.1 x.2.2)

Uses 1 · Used by 7

Statement usesReference-allele indicator for a genotype copy

Used byAllele-copy observations of a genotype matrix · Decomposition of the admixture EM objective · The EM log-likelihood of the allele copies is the admixture log-likelihood · Ancestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities · Sum over allele-copy data as a triple sum · Admixture responsibilities sum to one

DefinitionPolymorphic genotype data#✓fully proved

Every SNP is polymorphic in the sample: some individual carries a reference allele and some individual carries an alternative allele. Without it the M-step frequency is 0 or 1.

def Polymorphic (g : I → J → Fin 3) : Prop := ∀ j, (∃ i, g i j ≠ 0) ∧ ∃ i, g i j ≠ 2

Used by 9

Used byThe admixture log-likelihood is monotone along the FRAPPE EM iterates · Each FRAPPE EM step does not decrease the admixture log-likelihood · Positivity of expected alternative counts on polymorphic data · The FRAPPE update maximizes Q(· | θ) · The FRAPPE EM step · Updated allele frequencies are less than one · Positivity of the updated allele frequencies · Positivity of expected population counts on polymorphic data · Positivity of expected reference counts on polymorphic data

DefinitionAllele-copy observations of a genotype matrix#✓fully proved

The 2 |I| |J| allele-copy observations of the genotype matrix g, indexed by Fin.

noncomputable def data (g : I → J → Fin 3) :
    Fin (Fintype.card (I × J × Fin 2)) → I × J × Bool :=
  fun n => copyAllele g ((Fintype.equivFin _).symm n)

Uses 1 · Used by 6

Statement usesObservation of one allele copy of a genotype

Used byThe admixture log-likelihood is monotone along the iterates · The EM theorem for the admixture model · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · The EM log-likelihood of the allele copies is the admixture log-likelihood · Sum over allele-copy data as a triple sum

TheoremSum over allele-copy data as a triple sum#✓fully proved

A sum over the indexed data is a sum over individuals, SNPs and copies.

theorem sum_data (g : I → J → Fin 3) (f : I × J × Bool → ℝ) :
    ∑ n, f (data g n) = ∑ i, ∑ j, ∑ c : Fin 2, f (copyAllele g (i, j, c))

Uses 2 · Used by 2

Statement usesObservation of one allele copy of a genotype · Allele-copy observations of a genotype matrix

Used byDecomposition of the admixture EM objective · The EM log-likelihood of the allele copies is the admixture log-likelihood

DefinitionAdmixture log-likelihood#✓fully proved

The admixture log-likelihood ℓ(Q, F) = ∑ i, ∑ j, (g i j * log (qf θ i j) + (2 - g i j) * log (1 - qf θ i j)).

noncomputable def admixtureLogLik (g : I → J → Fin 3) (θ : Params I J K) : ℝ :=
  ∑ i, ∑ j, (((g i j).val : ℝ) * log (qf θ i j) + (2 - ((g i j).val : ℝ)) * log (1 - qf θ i j))

Uses 2 · Used by 5

Statement usesParameters of the admixture model · Reference-allele probability in the admixture model

Used byThe admixture log-likelihood is monotone along the FRAPPE EM iterates · The admixture log-likelihood is monotone along the iterates · Each FRAPPE EM step does not decrease the admixture log-likelihood · The EM theorem for the admixture model · The EM log-likelihood of the allele copies is the admixture log-likelihood

TheoremThe EM log-likelihood of the allele copies is the admixture log-likelihood#✓fully proved

The EM log-likelihood of the allele copies is the admixture log-likelihood.

theorem logLik_eq_admixtureLogLik (g : I → J → Fin 3) (θ : Params I J K) :
    logLik joint (data g) θ = admixtureLogLik g θ

Uses 10 · Used by 2

Statement usesParameters of the admixture model · Admixture log-likelihood · Allele-copy observations of a genotype matrix · Joint weight of an allele copy and its ancestral population · Log-likelihood of a latent-variable model

Proof usesObservation of one allele copy of a genotype · The marginal of an allele copy · Reference-allele probability in the admixture model · Sum over allele-copy data as a triple sum · Marginal of a latent-variable model

Used byThe admixture log-likelihood is monotone along the iterates · The EM theorem for the admixture model

The EM theorem

TheoremThe EM theorem for the admixture model#✓fully proved

A step that does not decrease Q(· | θ) does not decrease the admixture log-likelihood.

theorem admixtureLogLik_le_of_emQ_le [Nonempty K] (g : I → J → Fin 3) {θ θ' : Params I J K}
    (h : emQ joint (data g) θ θ ≤ emQ joint (data g) θ' θ) :
    admixtureLogLik g θ ≤ admixtureLogLik g θ'

Uses 9 · Used by 1

Statement usesParameters of the admixture model · Admixture log-likelihood · Allele-copy observations of a genotype matrix · Joint weight of an allele copy and its ancestral population · The EM objective

Proof usesPositivity of the admixture joint weight · The EM log-likelihood of the allele copies is the admixture log-likelihood · Log-likelihood of a latent-variable model · The EM theorem

Used byEach FRAPPE EM step does not decrease the admixture log-likelihood

TheoremThe admixture log-likelihood is monotone along the iterates#✓fully proved

The admixture log-likelihood is monotone along the iterates of any M-step M with Q(M θ | θ) ≥ Q(θ | θ).

theorem admixtureLogLik_iterate_monotone [Nonempty K] (g : I → J → Fin 3)
    {M : Params I J K → Params I J K}
    (hM : ∀ θ, emQ joint (data g) θ θ ≤ emQ joint (data g) (M θ) θ)
    (θ₀ : Params I J K) : Monotone fun t => admixtureLogLik g (M^[t] θ₀)

Uses 9 · Used by 1

Statement usesParameters of the admixture model · Admixture log-likelihood · Allele-copy observations of a genotype matrix · Joint weight of an allele copy and its ancestral population · The EM objective

Proof usesPositivity of the admixture joint weight · The EM log-likelihood of the allele copies is the admixture log-likelihood · Log-likelihood of a latent-variable model · EM iterates have monotone likelihood

Used byThe admixture log-likelihood is monotone along the FRAPPE EM iterates

The closed-form M-step

DefinitionAncestry responsibility of an allele copy (E-step)#✓fully proved

The responsibility r = P(z = k | copy c of (i, j)) (the E-step).

noncomputable def resp (θ : Params I J K) (i : I) (j : J) (c : Fin 2) (k : K) : ℝ :=
  posterior joint θ (copyAllele g (i, j, c)) k

Uses 4 · Used by 12

Statement usesParameters of the admixture model · Observation of one allele copy of a genotype · Joint weight of an allele copy and its ancestral population · Posterior of a latent-variable model

Used byExpected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Expected ancestry count of an individual · Positivity of the expected ancestry counts · Decomposition of the admixture EM objective · Expected population count of a SNP · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data · Positivity of the admixture responsibilities · Expected ancestry counts sum to the number of allele copies · Admixture responsibilities sum to one

TheoremPositivity of the admixture responsibilities#✓fully proved

The responsibilities are positive.

theorem resp_pos (θ : Params I J K) (i : I) (j : J) (c : Fin 2) (k : K) :
    0 < resp g θ i j c k

Uses 6 · Used by 3

Statement usesParameters of the admixture model · Ancestry responsibility of an allele copy (E-step)

Proof usesObservation of one allele copy of a genotype · Joint weight of an allele copy and its ancestral population · Positivity of the admixture joint weight · Marginal of a latent-variable model

Used byPositivity of expected alternative counts on polymorphic data · Positivity of the expected ancestry counts · Positivity of expected reference counts on polymorphic data

TheoremAdmixture responsibilities sum to one#✓fully proved

The responsibilities of a copy sum to one over the populations.

theorem sum_resp [Nonempty K] (θ : Params I J K) (i : I) (j : J) (c : Fin 2) :
    ∑ k, resp g θ i j c k = 1

Uses 7 · Used by 1

Statement usesParameters of the admixture model · Ancestry responsibility of an allele copy (E-step)

Proof usesObservation of one allele copy of a genotype · Joint weight of an allele copy and its ancestral population · Positivity of the admixture joint weight · Posteriors are probability distributions · Posterior of a latent-variable model

Used byExpected ancestry counts sum to the number of allele copies

DefinitionExpected ancestry count of an individual#✓fully proved

The expected number of allele copies of individual i from population k.

noncomputable def ancCount (θ : Params I J K) (i : I) (k : K) : ℝ :=
  ∑ j, ∑ c, resp g θ i j c k

Uses 2 · Used by 7

Statement usesParameters of the admixture model · Ancestry responsibility of an allele copy (E-step)

Used byPositivity of the expected ancestry counts · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · FRAPPE update of the ancestry proportions · Positivity of the updated ancestry proportions · Updated ancestry proportions sum to one · Expected ancestry counts sum to the number of allele copies

DefinitionFRAPPE update of the ancestry proportions#✓fully proved

The FRAPPE update of the ancestry proportions, Q' i k = (∑ j, ∑ c, r) / (2 J).

noncomputable def mStepQ (θ : Params I J K) (i : I) (k : K) : ℝ :=
  ancCount g θ i k / (2 * Fintype.card J)

Uses 2 · Used by 3

Statement usesParameters of the admixture model · Expected ancestry count of an individual

Used byThe FRAPPE EM step · Positivity of the updated ancestry proportions · Updated ancestry proportions sum to one

TheoremExpected ancestry counts sum to the number of allele copies#✓fully proved

The expected ancestry counts of an individual sum to its 2 J allele copies.

theorem sum_ancCount [Nonempty K] (θ : Params I J K) (i : I) :
    ∑ k, ancCount g θ i k = 2 * Fintype.card J

Uses 4 · Used by 2

Statement usesParameters of the admixture model · Expected ancestry count of an individual

Proof usesAncestry responsibility of an allele copy (E-step) · Admixture responsibilities sum to one

Used byThe FRAPPE update maximizes Q(· | θ) · Updated ancestry proportions sum to one

TheoremPositivity of the expected ancestry counts#✓fully proved

The expected ancestry counts are positive when there is at least one SNP.

theorem ancCount_pos [Nonempty J] (θ : Params I J K) (i : I) (k : K) : 0 < ancCount g θ i k

Uses 4 · Used by 2

Statement usesParameters of the admixture model · Expected ancestry count of an individual

Proof usesAncestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities

Used byThe FRAPPE update maximizes Q(· | θ) · Positivity of the updated ancestry proportions

TheoremPositivity of the updated ancestry proportions#✓fully proved

The updated ancestry proportions are positive.

theorem mStep_Q_pos [Nonempty J] (θ : Params I J K) (i : I) (k : K) : 0 < mStepQ g θ i k

Uses 4 · Used by 1

Statement usesParameters of the admixture model · FRAPPE update of the ancestry proportions

Proof usesExpected ancestry count of an individual · Positivity of the expected ancestry counts

Used byThe FRAPPE EM step

TheoremUpdated ancestry proportions sum to one#✓fully proved

The updated ancestry proportions of each individual sum to one.

theorem mStep_Q_sum [Nonempty J] [Nonempty K] (θ : Params I J K) (i : I) :
    ∑ k, mStepQ g θ i k = 1

Uses 4 · Used by 1

Statement usesParameters of the admixture model · FRAPPE update of the ancestry proportions

Proof usesExpected ancestry count of an individual · Expected ancestry counts sum to the number of allele copies

Used byThe FRAPPE EM step

DefinitionExpected population count of a SNP#✓fully proved

The expected number of allele copies of SNP j from population k.

noncomputable def popCount (θ : Params I J K) (k : K) (j : J) : ℝ :=
  ∑ i, ∑ c, resp g θ i j c k

Uses 2 · Used by 6

Statement usesParameters of the admixture model · Ancestry responsibility of an allele copy (E-step)

Used byThe FRAPPE update maximizes Q(· | θ) · FRAPPE update of the allele frequencies · Updated allele frequencies are less than one · Positivity of the updated allele frequencies · Positivity of expected population counts on polymorphic data · Reference and alternative counts add to the population count

DefinitionExpected reference-allele count of a SNP per population#✓fully proved

The expected number of reference copies of SNP j from population k.

noncomputable def refCount (θ : Params I J K) (k : K) (j : J) : ℝ :=
  ∑ i, ∑ c, if isRef g i j c then resp g θ i j c k else 0

Uses 3 · Used by 8

Statement usesParameters of the admixture model · Reference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step)

Used byDecomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · FRAPPE update of the allele frequencies · Updated allele frequencies are less than one · Positivity of the updated allele frequencies · Positivity of expected population counts on polymorphic data · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data

DefinitionExpected alternative-allele count of a SNP per population#✓fully proved

The expected number of alternative copies of SNP j from population k.

noncomputable def altCount (θ : Params I J K) (k : K) (j : J) : ℝ :=
  ∑ i, ∑ c, if isRef g i j c then 0 else resp g θ i j c k

Uses 3 · Used by 6

Statement usesParameters of the admixture model · Reference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step)

Used byPositivity of expected alternative counts on polymorphic data · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · Updated allele frequencies are less than one · Positivity of expected population counts on polymorphic data · Reference and alternative counts add to the population count

DefinitionFRAPPE update of the allele frequencies#✓fully proved

The FRAPPE update of the allele frequencies, F' k j = (∑ i, ∑ c reference, r) / (∑ i, ∑ c, r).

noncomputable def mStepF (θ : Params I J K) (k : K) (j : J) : ℝ :=
  refCount g θ k j / popCount g θ k j

Uses 3 · Used by 3

Statement usesParameters of the admixture model · Expected population count of a SNP · Expected reference-allele count of a SNP per population

Used byThe FRAPPE EM step · Updated allele frequencies are less than one · Positivity of the updated allele frequencies

TheoremReference and alternative counts add to the population count#✓fully proved

Reference plus alternative expected counts give the population's expected count.

theorem refCount_add_altCount (θ : Params I J K) (k : K) (j : J) :
    refCount g θ k j + altCount g θ k j = popCount g θ k j

Uses 6 · Used by 3

Statement usesParameters of the admixture model · Expected alternative-allele count of a SNP per population · Expected population count of a SNP · Expected reference-allele count of a SNP per population

Proof usesReference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step)

Used byThe FRAPPE update maximizes Q(· | θ) · Updated allele frequencies are less than one · Positivity of expected population counts on polymorphic data

TheoremPositivity of expected reference counts on polymorphic data#✓fully proved

On polymorphic data the expected reference counts are positive.

theorem refCount_pos (hg : Polymorphic g) (θ : Params I J K) (k : K) (j : J) :
    0 < refCount g θ k j

Uses 6 · Used by 3

Statement usesParameters of the admixture model · Polymorphic genotype data · Expected reference-allele count of a SNP per population

Proof usesReference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities

Used byThe FRAPPE update maximizes Q(· | θ) · Positivity of the updated allele frequencies · Positivity of expected population counts on polymorphic data

TheoremPositivity of expected alternative counts on polymorphic data#✓fully proved

On polymorphic data the expected alternative counts are positive.

theorem altCount_pos (hg : Polymorphic g) (θ : Params I J K) (k : K) (j : J) :
    0 < altCount g θ k j

Uses 6 · Used by 3

Statement usesParameters of the admixture model · Polymorphic genotype data · Expected alternative-allele count of a SNP per population

Proof usesReference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step) · Positivity of the admixture responsibilities

Used byThe FRAPPE update maximizes Q(· | θ) · Updated allele frequencies are less than one · Positivity of expected population counts on polymorphic data

TheoremPositivity of expected population counts on polymorphic data#✓fully proved

On polymorphic data the expected population counts are positive.

theorem popCount_pos (hg : Polymorphic g) (θ : Params I J K) (k : K) (j : J) :
    0 < popCount g θ k j

Uses 8 · Used by 3

Statement usesParameters of the admixture model · Polymorphic genotype data · Expected population count of a SNP

Proof usesExpected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data

Used byThe FRAPPE update maximizes Q(· | θ) · Updated allele frequencies are less than one · Positivity of the updated allele frequencies

TheoremPositivity of the updated allele frequencies#✓fully proved

On polymorphic data the updated allele frequencies are positive.

theorem mStep_F_pos (hg : Polymorphic g) (θ : Params I J K) (k : K) (j : J) :
    0 < mStepF g θ k j

Uses 7 · Used by 1

Statement usesParameters of the admixture model · Polymorphic genotype data · FRAPPE update of the allele frequencies

Proof usesExpected population count of a SNP · Positivity of expected population counts on polymorphic data · Expected reference-allele count of a SNP per population · Positivity of expected reference counts on polymorphic data

Used byThe FRAPPE EM step

TheoremUpdated allele frequencies are less than one#✓fully proved

On polymorphic data the updated allele frequencies are below one.

theorem mStep_F_lt_one (hg : Polymorphic g) (θ : Params I J K) (k : K) (j : J) :
    mStepF g θ k j < 1

Uses 9 · Used by 1

Statement usesParameters of the admixture model · Polymorphic genotype data · FRAPPE update of the allele frequencies

Proof usesExpected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Expected population count of a SNP · Positivity of expected population counts on polymorphic data · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count

Used byThe FRAPPE EM step

DefinitionThe FRAPPE EM step#✓fully proved

The FRAPPE EM step θ ↦ (Q', F'), with Q' = mStepQ and F' = mStepF; it lies in the strictly positive parameter set when J is nonempty and every SNP is polymorphic.

noncomputable def emStep [Nonempty J] [Nonempty K] (hg : Polymorphic g) (θ : Params I J K) :
    Params I J K where
  Q := mStepQ g θ
  F := mStepF g θ
  Q_pos := mStep_Q_pos θ
  Q_sum := mStep_Q_sum θ
  F_pos := mStep_F_pos hg θ
  F_lt_one := mStep_F_lt_one hg θ

Uses 8 · Used by 3

Statement usesParameters of the admixture model · Polymorphic genotype data · FRAPPE update of the allele frequencies · FRAPPE update of the ancestry proportions · Updated allele frequencies are less than one · Positivity of the updated allele frequencies · Positivity of the updated ancestry proportions · Updated ancestry proportions sum to one

Used byThe admixture log-likelihood is monotone along the FRAPPE EM iterates · Each FRAPPE EM step does not decrease the admixture log-likelihood · The FRAPPE update maximizes Q(· | θ)

The M-step maximizes Q

TheoremDecomposition of the admixture EM objective#✓fully proved

Q(θ' | θ) splits into an ancestry term per individual and a two-point term per population and SNP.

theorem emQ_eq (θ' θ : Params I J K) :
    emQ joint (data g) θ' θ = ∑ i, ∑ k, ancCount g θ i k * log (θ'.Q i k) +
      ∑ k, ∑ j, (refCount g θ k j * log (θ'.F k j) +
        altCount g θ k j * log (1 - θ'.F k j))

Uses 12 · Used by 1

Statement usesParameters of the admixture model · Expected alternative-allele count of a SNP per population · Expected ancestry count of an individual · Allele-copy observations of a genotype matrix · Joint weight of an allele copy and its ancestral population · Expected reference-allele count of a SNP per population · The EM objective

Proof usesObservation of one allele copy of a genotype · Reference-allele indicator for a genotype copy · Ancestry responsibility of an allele copy (E-step) · Sum over allele-copy data as a triple sum · Posterior of a latent-variable model

Used byThe FRAPPE update maximizes Q(· | θ)

TheoremThe FRAPPE update maximizes Q(· | θ)#✓fully proved

No parameter θ' in the strictly positive parameter set has a larger Q(θ' | θ) than the closed-form update emStep g hg θ.

theorem emQ_le_emStep [Nonempty J] [Nonempty K] (hg : Polymorphic g) (θ' θ : Params I J K) :
    emQ joint (data g) θ' θ ≤ emQ joint (data g) (emStep g hg θ) θ

Uses 18 · Used by 2

Statement usesParameters of the admixture model · Polymorphic genotype data · Allele-copy observations of a genotype matrix · The FRAPPE EM step · Joint weight of an allele copy and its ancestral population · The EM objective

Proof usesExpected alternative-allele count of a SNP per population · Positivity of expected alternative counts on polymorphic data · Expected ancestry count of an individual · Positivity of the expected ancestry counts · Decomposition of the admixture EM objective · Expected population count of a SNP · Positivity of expected population counts on polymorphic data · Expected reference-allele count of a SNP per population · Reference and alternative counts add to the population count · Positivity of expected reference counts on polymorphic data · Expected ancestry counts sum to the number of allele copies · The weighted log-likelihood is bounded by its value at the normalized counts

Used byThe admixture log-likelihood is monotone along the FRAPPE EM iterates · Each FRAPPE EM step does not decrease the admixture log-likelihood

TheoremEach FRAPPE EM step does not decrease the admixture log-likelihood#✓fully proved

Each FRAPPE EM step does not decrease the admixture log-likelihood.

theorem admixtureLogLik_le_emStep [Nonempty J] [Nonempty K] (hg : Polymorphic g)
    (θ : Params I J K) : admixtureLogLik g θ ≤ admixtureLogLik g (emStep g hg θ)

Uses 6

Statement usesParameters of the admixture model · Polymorphic genotype data · Admixture log-likelihood · The FRAPPE EM step

Proof usesThe EM theorem for the admixture model · The FRAPPE update maximizes Q(· | θ)

TheoremThe admixture log-likelihood is monotone along the FRAPPE EM iterates#✓fully proved

The admixture log-likelihood is monotone along the FRAPPE EM iterates.

theorem admixtureLogLik_iterate_emStep_monotone [Nonempty J] [Nonempty K] (hg : Polymorphic g)
    (θ₀ : Params I J K) : Monotone fun t => admixtureLogLik g ((emStep g hg)^[t] θ₀)

Uses 6

Statement usesParameters of the admixture model · Polymorphic genotype data · Admixture log-likelihood · The FRAPPE EM step

Proof usesThe admixture log-likelihood is monotone along the iterates · The FRAPPE update maximizes Q(· | θ)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.