Wright–Fisher Markov chain

DefinitionNeutral Wright–Fisher transition matrix#✓fully proved

The neutral Wright–Fisher transition matrix on M gene copies (Ewens 2004, ch. 3): P(i, j) = (M choose j) (i/M)^j (1 - i/M)^(M - j), the binomial law Bin(M, i/M) of the number of A copies among M draws with replacement. The model needs M ≥ 1; for M = 0 (where i / M is Lean's junk value 0) the matrix is the one-state chain, which is Bin(0, p) = δ₀ for every p.

noncomputable def wrightFisher (M : ℕ) : StochasticMatrix M where
  prob i j := bernstein M j (bernstein.z i)
  nonneg _ _ := bernstein_nonneg
  row_sum i := bernstein.probability M (bernstein.z i)

Uses 1 · Used by 18

Statement usesStochastic matrix

Used byAlmost-sure absorption of the Wright–Fisher chain · Finite Wright–Fisher chain is absorbed almost surely · Fixation probability of a Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain · Geometric decay of heterozygosity under Wright–Fisher drift · Multi-step martingale property of the Wright–Fisher allele count · One-step decay of heterozygosity under Wright–Fisher drift · One-step martingale property of the Wright–Fisher allele count · Interior Wright–Fisher states vanish in the limit · Fixation probability in the Wright–Fisher chain · Limiting loss probability of the Wright–Fisher transition matrix · Limiting fixation probability of a Wright–Fisher chain · Entries of the Wright–Fisher matrix · Wright–Fisher rows are binomial laws · Fixation of an allele is absorbing in the Wright–Fisher chain · Loss of an allele is absorbing in the Wright–Fisher chain

TheoremAllele frequency of a Wright–Fisher state#✓fully proved

The frequency of allele A in state i is bernstein.z i = i / M (for M = 0 it is Lean's junk value i / 0 = 0).

theorem coe_z (M : ℕ) (i : Fin (M + 1)) : (bernstein.z i : ℝ) = ((i : ℕ) : ℝ) / M

Used by 2

Used byOne-step decay of heterozygosity under Wright–Fisher drift · One-step martingale property of the Wright–Fisher allele count

TheoremEntries of the Wright–Fisher matrix#✓fully proved

Entries of the Wright–Fisher matrix.

theorem wrightFisher_prob (M : ℕ) (i j : Fin (M + 1)) :
    (wrightFisher M).prob i j =
      (M.choose j : ℝ) * (bernstein.z i : ℝ) ^ (j : ℕ) * (1 - (bernstein.z i : ℝ)) ^ (M - j)

Uses 2 · Used by 5

Statement usesNeutral Wright–Fisher transition matrix · Stochastic matrix

Used byOne-step decay of heterozygosity under Wright–Fisher drift · One-step martingale property of the Wright–Fisher allele count · Wright–Fisher rows are binomial laws · Fixation of an allele is absorbing in the Wright–Fisher chain · Loss of an allele is absorbing in the Wright–Fisher chain

DefinitionHeterozygosity of a Wright–Fisher state#✓fully proved

The heterozygosity H(j) = 2 (j/M) (1 - j/M) of state j: the probability that two gene copies drawn with replacement carry different alleles.

noncomputable def heterozygosity (M : ℕ) (j : Fin (M + 1)) : ℝ :=
  2 * (bernstein.z j : ℝ) * (1 - (bernstein.z j : ℝ))

Used by 3

Used byGeometric decay of heterozygosity under Wright–Fisher drift · One-step decay of heterozygosity under Wright–Fisher drift · Interior Wright–Fisher states vanish in the limit

TheoremWright–Fisher rows are binomial laws#✓fully proved

The rows of the Wright–Fisher matrix are Mathlib's binomial laws Bin(M, i/M).

theorem wrightFisher_prob_eq_binomial (M : ℕ) (i j : Fin (M + 1)) :
    (wrightFisher M).prob i j =
      (ProbabilityTheory.binomial M (bernstein.z i)).real {(j : ℕ)}

Uses 3

Statement usesNeutral Wright–Fisher transition matrix · Stochastic matrix

Proof usesEntries of the Wright–Fisher matrix

TheoremOne-step martingale property of the Wright–Fisher allele count#✓fully proved

Martingale property of the allele count (one step): ∑ j, P(i, j) j = i.

theorem sum_prob_mul_wrightFisher (M : ℕ) (i : Fin (M + 1)) :
    ∑ j, (wrightFisher M).prob i j * ((j : ℕ) : ℝ) = (i : ℕ)

Uses 4 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Stochastic matrix

Proof usesAllele frequency of a Wright–Fisher state · Entries of the Wright–Fisher matrix

Used byMulti-step martingale property of the Wright–Fisher allele count

TheoremMulti-step martingale property of the Wright–Fisher allele count#✓fully proved

Martingale property of the allele count (t steps): ∑ j, P^t(i, j) j = i.

theorem sum_matPow_mul_wrightFisher (M t : ℕ) (i : Fin (M + 1)) :
    ∑ j, (wrightFisher M).matPow t i j * ((j : ℕ) : ℝ) = (i : ℕ)

Uses 4 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Matrix powers of a stochastic matrix

Proof usesOne-step martingale property of the Wright–Fisher allele count · Stochastic matrix

Used byFixation probability in the Wright–Fisher chain

TheoremLoss of an allele is absorbing in the Wright–Fisher chain#✓fully proved

The state 0 (allele A lost) is absorbing.

theorem wrightFisher_prob_zero_zero (M : ℕ) : (wrightFisher M).prob 0 0 = 1

Uses 3 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Stochastic matrix

Proof usesEntries of the Wright–Fisher matrix

Used byLoss probability of a Wright–Fisher chain

TheoremFixation of an allele is absorbing in the Wright–Fisher chain#✓fully proved

The state M (allele A fixed) is absorbing.

theorem wrightFisher_prob_last_last (M : ℕ) :
    (wrightFisher M).prob (Fin.last M) (Fin.last M) = 1

Uses 3 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Stochastic matrix

Proof usesEntries of the Wright–Fisher matrix

Used byFixation probability of a Wright–Fisher chain

TheoremOne-step decay of heterozygosity under Wright–Fisher drift#✓fully proved

Heterozygosity decays by the factor 1 - 1/M per generation (one step). For M = 0 both sides are 0 because H ≡ 0.

theorem sum_prob_mul_heterozygosity (M : ℕ) (i : Fin (M + 1)) :
    ∑ j, (wrightFisher M).prob i j * heterozygosity M j =
      (1 - 1 / (M : ℝ)) * heterozygosity M i

Uses 5 · Used by 1

Statement usesHeterozygosity of a Wright–Fisher state · Neutral Wright–Fisher transition matrix · Stochastic matrix

Proof usesAllele frequency of a Wright–Fisher state · Entries of the Wright–Fisher matrix

Used byGeometric decay of heterozygosity under Wright–Fisher drift

TheoremGeometric decay of heterozygosity under Wright–Fisher drift#✓fully proved

Heterozygosity decays geometrically (Ewens 2004, ch. 3): ∑ j, P^t(i, j) H(j) = (1 - 1/M)^t H(i). For M = 0 both sides are 0 because H ≡ 0 (the factor 1 - 1/0 = 1 is then irrelevant).

theorem sum_matPow_mul_heterozygosity (M t : ℕ) (i : Fin (M + 1)) :
    ∑ j, (wrightFisher M).matPow t i j * heterozygosity M j =
      (1 - 1 / (M : ℝ)) ^ t * heterozygosity M i

Uses 5 · Used by 1

Statement usesHeterozygosity of a Wright–Fisher state · Neutral Wright–Fisher transition matrix · Matrix powers of a stochastic matrix

Proof usesOne-step decay of heterozygosity under Wright–Fisher drift · Stochastic matrix

Used byInterior Wright–Fisher states vanish in the limit

TheoremInterior Wright–Fisher states vanish in the limit#✓fully proved

The probability of sitting in an interior state 0 < j < M at time t tends to 0.

theorem tendsto_matPow_interior {M : ℕ} (i j : Fin (M + 1)) (hj0 : j ≠ 0)
    (hjM : j ≠ Fin.last M) :
    Tendsto (fun t => (wrightFisher M).matPow t i j) atTop (𝓝 0)

Uses 5 · Used by 2

Statement usesNeutral Wright–Fisher transition matrix · Matrix powers of a stochastic matrix

Proof usesHeterozygosity of a Wright–Fisher state · Geometric decay of heterozygosity under Wright–Fisher drift · Powers of a stochastic matrix are nonnegative

Used byFixation probability in the Wright–Fisher chain · Limiting loss probability of the Wright–Fisher transition matrix

TheoremFixation probability in the Wright–Fisher chain#✓fully proved

Fixation probability (Ewens 2004, ch. 3): started from i copies, allele A is fixed with limiting probability i / M, i.e. P^t(i, M) → i / M.

theorem tendsto_matPow_last {M : ℕ} (hM : 0 < M) (i : Fin (M + 1)) :
    Tendsto (fun t => (wrightFisher M).matPow t i (Fin.last M)) atTop
      (𝓝 (((i : ℕ) : ℝ) / M))

Uses 4 · Used by 3

Statement usesNeutral Wright–Fisher transition matrix · Matrix powers of a stochastic matrix

Proof usesMulti-step martingale property of the Wright–Fisher allele count · Interior Wright–Fisher states vanish in the limit

Used byAlmost-sure absorption of the Wright–Fisher chain · Limiting loss probability of the Wright–Fisher transition matrix · Limiting fixation probability of a Wright–Fisher chain

TheoremLimiting loss probability of the Wright–Fisher transition matrix#✓fully proved

Loss probability: started from i copies, allele A is lost with limiting probability 1 - i / M, i.e. P^t(i, 0) → 1 - i / M.

theorem tendsto_matPow_zero {M : ℕ} (hM : 0 < M) (i : Fin (M + 1)) :
    Tendsto (fun t => (wrightFisher M).matPow t i 0) atTop
      (𝓝 (1 - ((i : ℕ) : ℝ) / M))

Uses 5 · Used by 2

Statement usesNeutral Wright–Fisher transition matrix · Matrix powers of a stochastic matrix

Proof usesInterior Wright–Fisher states vanish in the limit · Fixation probability in the Wright–Fisher chain · Powers of a stochastic matrix are stochastic

Used byAlmost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain

TheoremLimiting fixation probability of a Wright–Fisher chain#✓fully proved

Path-level fixation probability: if X is a Wright–Fisher chain (in the sense of IsFiniteMarkovChain) started from i copies, then P(X_t = M) → i / M.

theorem tendsto_measureReal_eq_last {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {M : ℕ} (hM : 0 < M) {X : ℕ → Ω → Fin (M + 1)}
    {ℱ : MeasureTheory.Filtration ℕ m} (hX : IsFiniteMarkovChain X (wrightFisher M) ℱ μ)
    {i : Fin (M + 1)} (h0 : ∀ᵐ ω ∂μ, X 0 ω = i) :
    Tendsto (fun t => μ.real {ω | X t ω = Fin.last M}) atTop (𝓝 (((i : ℕ) : ℝ) / M))

Uses 11 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Finite-state Markov chain with a given transition matrix

Proof usesFixation probability in the Wright–Fisher chain · One-step forward equation · Transition kernel of a stochastic matrix · Transition kernel of a stochastic matrix evaluated on a set · Stochastic matrix · Matrix powers of a stochastic matrix · Additivity of recursive matrix powers · Powers of a stochastic matrix are nonnegative · First recursive power of a stochastic matrix

Used byFixation probability of a Wright–Fisher chain

TheoremAlmost-sure absorption of the Wright–Fisher chain#✓fully proved

Almost-sure absorption: a Wright–Fisher chain is almost surely eventually absorbed in 0 or M (Ewens 2004, ch. 3).

theorem measure_exists_absorbed {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {M : ℕ} {X : ℕ → Ω → Fin (M + 1)}
    {ℱ : MeasureTheory.Filtration ℕ m} (hX : IsFiniteMarkovChain X (wrightFisher M) ℱ μ)
    {i : Fin (M + 1)} (h0 : ∀ᵐ ω ∂μ, X 0 ω = i) :
    μ {ω | ∃ t, X t ω = 0 ∨ X t ω = Fin.last M} = 1

Uses 12 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Finite-state Markov chain with a given transition matrix

Proof usesFixation probability in the Wright–Fisher chain · Limiting loss probability of the Wright–Fisher transition matrix · One-step forward equation · Transition kernel of a stochastic matrix · Transition kernel of a stochastic matrix evaluated on a set · Stochastic matrix · Matrix powers of a stochastic matrix · Additivity of recursive matrix powers · Powers of a stochastic matrix are nonnegative · First recursive power of a stochastic matrix

Used byFinite Wright–Fisher chain is absorbed almost surely

TheoremFixation probability of a Wright–Fisher chain#✓fully proved

Path-level fixation probability (Ewens 2004, ch. 3): a Wright–Fisher chain started from i copies ever reaches M (fixation of A) with probability i / M.

theorem measureReal_exists_eq_last {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {M : ℕ} (hM : 0 < M) {X : ℕ → Ω → Fin (M + 1)}
    {ℱ : MeasureTheory.Filtration ℕ m} (hX : IsFiniteMarkovChain X (wrightFisher M) ℱ μ)
    {i : Fin (M + 1)} (h0 : ∀ᵐ ω ∂μ, X 0 ω = i) :
    μ.real {ω | ∃ t, X t ω = Fin.last M} = ((i : ℕ) : ℝ) / M

Uses 5 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Finite-state Markov chain with a given transition matrix

Proof usesLimiting fixation probability of a Wright–Fisher chain · Fixation of an allele is absorbing in the Wright–Fisher chain · Stochastic matrix

Used byFixation probability of the finite Wright–Fisher chain

TheoremLoss probability of a Wright–Fisher chain#✓fully proved

Path-level loss probability: a Wright–Fisher chain started from i copies ever reaches 0 (loss of A) with probability 1 - i / M.

theorem measureReal_exists_eq_zero {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {M : ℕ} (hM : 0 < M) {X : ℕ → Ω → Fin (M + 1)}
    {ℱ : MeasureTheory.Filtration ℕ m} (hX : IsFiniteMarkovChain X (wrightFisher M) ℱ μ)
    {i : Fin (M + 1)} (h0 : ∀ᵐ ω ∂μ, X 0 ω = i) :
    μ.real {ω | ∃ t, X t ω = 0} = 1 - ((i : ℕ) : ℝ) / M

Uses 12 · Used by 1

Statement usesNeutral Wright–Fisher transition matrix · Finite-state Markov chain with a given transition matrix

Proof usesLimiting loss probability of the Wright–Fisher transition matrix · Loss of an allele is absorbing in the Wright–Fisher chain · One-step forward equation · Transition kernel of a stochastic matrix · Transition kernel of a stochastic matrix evaluated on a set · Stochastic matrix · Matrix powers of a stochastic matrix · Additivity of recursive matrix powers · Powers of a stochastic matrix are nonnegative · First recursive power of a stochastic matrix

Used byLoss probability of an allele in the finite Wright–Fisher chain

TheoremFinite Wright–Fisher chain is absorbed almost surely#✓fully proved

The finite Wright–Fisher chain under the canonical Markov law almost surely reaches an endpoint. The law and chain are not premises supplied by a caller.

theorem measure_markovChainMeasure_exists_absorbed (M : ℕ) (i : Fin (M + 1)) :
    (markovChainMeasure (finiteChainKernel (wrightFisher M)) (Measure.dirac i))
      {ω | ∃ t, ω t = 0 ∨ ω t = Fin.last M} = 1

Uses 8

Statement usesNeutral Wright–Fisher transition matrix · Transition kernel of a stochastic matrix · Canonical Markov chain measure · Stochastic matrix

Proof usesAlmost-sure absorption of the Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Lifting a kernel to histories

TheoremFixation probability of the finite Wright–Fisher chain#✓fully proved

Under the canonical finite Wright–Fisher law, the probability of ever fixing at M equals the initial allele frequency i / M.

theorem measureReal_markovChainMeasure_exists_eq_last {M : ℕ} (hM : 0 < M)
    (i : Fin (M + 1)) :
    (markovChainMeasure (finiteChainKernel (wrightFisher M)) (Measure.dirac i)).real
      {ω | ∃ t, ω t = Fin.last M} = ((i : ℕ) : ℝ) / M

Uses 8

Statement usesNeutral Wright–Fisher transition matrix · Transition kernel of a stochastic matrix · Canonical Markov chain measure · Stochastic matrix

Proof usesFixation probability of a Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Lifting a kernel to histories

TheoremLoss probability of an allele in the finite Wright–Fisher chain#✓fully proved

Under the canonical finite Wright–Fisher law, the probability of ever losing the allele at 0 equals 1 - i / M.

theorem measureReal_markovChainMeasure_exists_eq_zero {M : ℕ} (hM : 0 < M)
    (i : Fin (M + 1)) :
    (markovChainMeasure (finiteChainKernel (wrightFisher M)) (Measure.dirac i)).real
      {ω | ∃ t, ω t = 0} = 1 - ((i : ℕ) : ℝ) / M

Uses 8

Statement usesNeutral Wright–Fisher transition matrix · Transition kernel of a stochastic matrix · Canonical Markov chain measure · Stochastic matrix

Proof usesLoss probability of a Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Lifting a kernel to histories

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.