Li–Stephens haplotype copying model

AbbreviationSite observation in the Li–Stephens model#✓fully proved

The observation at a site: the column of reference alleles and the target allele.

abbrev Obs (K : ℕ) (A : Type*) := (Fin K → A) × A

Used by 13

Used byLi–Stephens emission probability · Forward variables of the collapsed recursion · The collapsed forward recursion computes the forward variables · Tabulated O(K) forward variables · Tabulated recursion computes the Li–Stephens forward variables · One step of the collapsed forward recursion · Tabulated O(K) forward step · The Li–Stephens copying model · Uniform initial law over haplotypes sums to one · The likelihood of the target haplotype · The tabulated Li–Stephens likelihood · Tabulated recursion computes the haplotype likelihood · Observation sequence of a reference panel and target haplotype

DefinitionObservation sequence of a reference panel and target haplotype#✓fully proved

The observation sequence for the reference panel H (haplotype k carries allele H k t at site t) and the target haplotype x.

def obs (H : Fin K → ℕ → A) (x : ℕ → A) (t : ℕ) : Obs K A := (fun k => H k t, x t)

Uses 1

Statement usesSite observation in the Li–Stephens model

DefinitionLi–Stephens copying transition probability#✓fully proved

The copying transition probability: switch with probability ρ to a uniformly random reference haplotype (possibly the same one), otherwise keep copying k: (1 - ρ) [k = k'] + ρ / K.

def trans (ρ : R) (k k' : Fin K) : R := (1 - ρ) * (if k = k' then 1 else 0) + ρ / K

Used by 4

Used byThe collapsed forward recursion computes the forward variables · The Li–Stephens copying model · Collapse of the sum over predecessor haplotypes · Li–Stephens transition rows sum to one

DefinitionLi–Stephens emission probability#✓fully proved

The emission probability: 1 - ε if the target allele equals the allele of the copied haplotype k, and the mismatch probability ε otherwise.

def emit (ε : R) (k : Fin K) (o : Obs K A) : R := if o.1 k = o.2 then 1 - ε else ε

Uses 1 · Used by 8

Statement usesSite observation in the Li–Stephens model

Used byBiallelic emission probabilities sum to one · Forward variables of the collapsed recursion · The collapsed forward recursion computes the forward variables · Tabulated O(K) forward variables · Tabulated recursion computes the Li–Stephens forward variables · One step of the collapsed forward recursion · Tabulated O(K) forward step · The Li–Stephens copying model

DefinitionThe Li–Stephens copying model#✓fully proved

The Li–Stephens copying model with K reference haplotypes, switch probability ρ and mismatch probability ε, as a hidden Markov model with a uniform initial copied haplotype.

def hmm (K : ℕ) (ρ ε : R) : HMM (Fin K) (Obs K A) R where
  init _ := 1 / K
  trans := trans ρ
  emit := emit ε

Uses 4 · Used by 5

Statement usesSite observation in the Li–Stephens model · Li–Stephens emission probability · Li–Stephens copying transition probability · Hidden Markov model

Used byThe collapsed forward recursion computes the forward variables · Tabulated recursion computes the Li–Stephens forward variables · Uniform initial law over haplotypes sums to one · The likelihood of the target haplotype · Tabulated recursion computes the haplotype likelihood

TheoremLi–Stephens transition rows sum to one#✓fully proved

Each transition row sums to 1 (when K is invertible in R, e.g. K ≠ 0 over ℝ).

theorem trans_row_sum (hK : (K : R) ≠ 0) (ρ : R) (k : Fin K) : ∑ k', trans ρ k k' = 1

Uses 1

Statement usesLi–Stephens copying transition probability

TheoremUniform initial law over haplotypes sums to one#✓fully proved

The initial law (uniform over the K haplotypes) sums to 1.

theorem init_sum (hK : (K : R) ≠ 0) (ρ ε : R) :
    ∑ k, (hmm (A := A) K ρ ε).init k = 1

Uses 3

Statement usesSite observation in the Li–Stephens model · The Li–Stephens copying model · Hidden Markov model

TheoremBiallelic emission probabilities sum to one#✓fully proved

With biallelic sites, the two emission probabilities at a site sum to 1 over the target allele, for each fixed panel column col (the emissions are conditional on the panel).

theorem emit_sum_bool (ε : R) (k : Fin K) (col : Fin K → Bool) :
    ∑ a : Bool, emit ε k (col, a) = 1

Uses 1

Statement usesLi–Stephens emission probability

DefinitionOne step of the collapsed forward recursion#✓fully proved

One step of the collapsed forward recursion on the previous site's forward variables v, at output state k: e_k ((1 - ρ) v k + ρ (∑ j, v j) / K). This is the pointwise specification; each call evaluates the length-K sum, so use fastStepTab for the O(K) per-site step.

def fastStep (ρ ε : R) (o : Obs K A) (v : Fin K → R) (k : Fin K) : R :=
  emit ε k o * ((1 - ρ) * v k + ρ * (∑ j, v j) / K)

Uses 2 · Used by 1

Statement usesSite observation in the Li–Stephens model · Li–Stephens emission probability

Used byForward variables of the collapsed recursion

DefinitionForward variables of the collapsed recursion#✓fully proved

The forward variables of the collapsed recursion, as a function of site and state. This is the untabulated specification (it re-evaluates earlier sites inside each sum); fastForwardTab is the O(t K) implementation.

def fastForward (ρ ε : R) (y : ℕ → Obs K A) : ℕ → Fin K → R
  | 0, k => 1 / K * emit ε k (y 0)
  | t + 1, k => fastStep ρ ε (y (t + 1)) (fastForward ρ ε y t) k

Uses 3 · Used by 3

Statement usesSite observation in the Li–Stephens model · Li–Stephens emission probability · One step of the collapsed forward recursion

Used byThe collapsed forward recursion computes the forward variables · Tabulated recursion computes the Li–Stephens forward variables · The likelihood of the target haplotype

TheoremCollapse of the sum over predecessor haplotypes#✓fully proved

The sum over predecessors collapses: ∑ j, v j * trans ρ j k = (1 - ρ) v k + ρ (∑ v) / K.

theorem sum_mul_trans (ρ : R) (v : Fin K → R) (k : Fin K) :
    ∑ j, v j * trans ρ j k = (1 - ρ) * v k + ρ * (∑ j, v j) / K

Uses 1 · Used by 1

Statement usesLi–Stephens copying transition probability

Used byThe collapsed forward recursion computes the forward variables

TheoremThe collapsed forward recursion computes the forward variables#✓fully proved

The collapsed forward recursion computes the forward variables of the Li–Stephens HMM.

theorem fastForward_eq_forward (ρ ε : R) (y : ℕ → Obs K A) :
    ∀ (t : ℕ) (k : Fin K), fastForward ρ ε y t k = forward (hmm K ρ ε) y t k

Uses 8 · Used by 2

Statement usesSite observation in the Li–Stephens model · Forward variables of the collapsed recursion · The Li–Stephens copying model · Forward variables of a hidden Markov model

Proof usesLi–Stephens emission probability · Collapse of the sum over predecessor haplotypes · Li–Stephens copying transition probability · Hidden Markov model

Used byTabulated recursion computes the Li–Stephens forward variables · The likelihood of the target haplotype

TheoremThe likelihood of the target haplotype#✓fully proved

The likelihood of the target haplotype (given the panel) is the sum of the collapsed forward variables.

theorem likelihood_eq_sum_fastForward (ρ ε : R) (y : ℕ → Obs K A) (t : ℕ) :
    likelihood (hmm K ρ ε) y t = ∑ k, fastForward ρ ε y t k

Uses 7

Statement usesSite observation in the Li–Stephens model · Forward variables of the collapsed recursion · The Li–Stephens copying model · Likelihood of the observations

Proof usesThe collapsed forward recursion computes the forward variables · Forward variables of a hidden Markov model · The forward algorithm computes the likelihood

DefinitionTabulated O(K) forward step#✓fully proved

One tabulated O(K) step: the total of the previous table is computed once.

def fastStepTab (ρ ε : R) (o : Obs K A) (v : Vector R K) : Vector R K :=
  let S := sumVec v
  Vector.ofFn fun k => emit ε k o * ((1 - ρ) * v[k] + ρ * S / K)

Uses 3 · Used by 1

Statement usesSite observation in the Li–Stephens model · Li–Stephens emission probability · Sum of the entries of a vector

Used byTabulated O(K) forward variables

DefinitionTabulated O(K) forward variables#✓fully proved

The O(K) forward variables, tabulated site by site: O(t K) operations in total.

def fastForwardTab (ρ ε : R) (y : ℕ → Obs K A) : ℕ → Vector R K
  | 0 => Vector.ofFn fun k => 1 / K * emit ε k (y 0)
  | t + 1 => fastStepTab ρ ε (y (t + 1)) (fastForwardTab ρ ε y t)

Uses 3 · Used by 3

Statement usesSite observation in the Li–Stephens model · Li–Stephens emission probability · Tabulated O(K) forward step

Used byTabulated recursion computes the Li–Stephens forward variables · The tabulated Li–Stephens likelihood · Tabulated recursion computes the haplotype likelihood

TheoremTabulated recursion computes the Li–Stephens forward variables#✓fully proved

The tabulated O(K) recursion computes the forward variables of the Li–Stephens HMM.

theorem fastForwardTab_get (ρ ε : R) (y : ℕ → Obs K A) :
    ∀ (t : ℕ) (k : Fin K), (fastForwardTab ρ ε y t)[k] = forward (hmm K ρ ε) y t k

Uses 7 · Used by 1

Statement usesSite observation in the Li–Stephens model · Tabulated O(K) forward variables · The Li–Stephens copying model · Forward variables of a hidden Markov model

Proof usesLi–Stephens emission probability · Forward variables of the collapsed recursion · The collapsed forward recursion computes the forward variables

Used byTabulated recursion computes the haplotype likelihood

DefinitionThe tabulated Li–Stephens likelihood#✓fully proved

The tabulated Li–Stephens likelihood in O(t K) operations.

def likelihoodTab (ρ ε : R) (y : ℕ → Obs K A) (t : ℕ) : R := sumVec (fastForwardTab ρ ε y t)

Uses 3 · Used by 1

Statement usesSite observation in the Li–Stephens model · Tabulated O(K) forward variables · Sum of the entries of a vector

Used byTabulated recursion computes the haplotype likelihood

TheoremTabulated recursion computes the haplotype likelihood#✓fully proved

The tabulated O(K) recursion computes the likelihood of the target haplotype.

theorem likelihoodTab_eq (ρ ε : R) (y : ℕ → Obs K A) (t : ℕ) :
    likelihoodTab ρ ε y t = likelihood (hmm K ρ ε) y t

Uses 9

Statement usesSite observation in the Li–Stephens model · The Li–Stephens copying model · The tabulated Li–Stephens likelihood · Likelihood of the observations

Proof usesTabulated O(K) forward variables · Tabulated recursion computes the Li–Stephens forward variables · Forward variables of a hidden Markov model · The forward algorithm computes the likelihood · Sum of the entries of a vector

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.