Haldane's survival probability of a beneficial mutation

TheoremGenerating function of the Poisson distribution#✓fully proved

The Poisson(r) generating function: ∑ e^{-r} r^k / k! x^k = exp (r (x - 1)).

theorem pgf_poissonMeasure (r : ℝ≥0) (x : ℝ) :
    pgf id (poissonMeasure r) x = exp (r * (x - 1))

Uses 1 · Used by 2

Statement usesProbability generating function

Used byHaldane's equation for the survival probability · Survival probability is less than one

TheoremMean of the Poisson distribution#✓fully proved

The Poisson(r) law has mean r.

theorem mean_poissonMeasure (r : ℝ≥0) : GaltonWatson.mean (poissonMeasure r) = r

Uses 1 · Used by 1

Statement usesMean offspring number

Used byBeneficial mutant survives with positive probability

DefinitionHaldane's survival probability of a mutant#✓fully proved

Haldane's survival probability π(s) = 1 - q(s) of a mutant with selective advantage s per generation, whose number of copies in the next generation is Poisson with mean 1 + s. The model needs s ≥ -1; for s < -1 the mean is truncated to 0 (Real.toNNReal), the mutant leaves no copies, and π(s) = 0.

noncomputable def survivalProb (s : ℝ) : ℝ :=
  1 - GaltonWatson.extinctionProb (poissonMeasure (1 + s).toNNReal)

Uses 1 · Used by 5

Statement usesExtinction probability of a Galton–Watson process

Used byHaldane's equation for the survival probability · Survival probability is less than one · Nonnegativity of the survival probability · Beneficial mutant survives with positive probability · Haldane's approximation \(\pi(s) \approx 2s\)

TheoremHaldane's equation for the survival probability#✓fully proved

π(s) solves Haldane's equation 1 - π = exp (-(1 + s) π).

theorem one_sub_survivalProb {s : ℝ} (hs : -1 ≤ s) :
    1 - survivalProb s = exp (-(1 + s) * survivalProb s)

Uses 5 · Used by 1

Statement usesHaldane's survival probability of a mutant

Proof usesGenerating function of the Poisson distribution · Extinction probability of a Galton–Watson process · Extinction probability is the least fixed point · Probability generating function

Used byHaldane's approximation \(\pi(s) \approx 2s\)

TheoremBeneficial mutant survives with positive probability#✓fully proved

A beneficial mutant survives with positive probability.

theorem survivalProb_pos {s : ℝ} (hs : 0 < s) : 0 < survivalProb s

Uses 7 · Used by 1

Statement usesHaldane's survival probability of a mutant

Proof usesMean of the Poisson distribution · Extinction probability of a Galton–Watson process · Galton–Watson extinction criterion · Extinction probability is the least fixed point · Mean offspring number · Probability generating function

Used byHaldane's approximation \(\pi(s) \approx 2s\)

TheoremSurvival probability is less than one#✓fully proved

The survival probability is less than 1: the mutant leaves no copies with positive probability exp (-(1 + s)). (For s < -1, outside the model, π(s) = 0.)

theorem survivalProb_lt_one (s : ℝ) : survivalProb s < 1

Uses 5 · Used by 1

Statement usesHaldane's survival probability of a mutant

Proof usesGenerating function of the Poisson distribution · Extinction probability of a Galton–Watson process · Extinction probability is the least fixed point · Probability generating function

Used byHaldane's approximation \(\pi(s) \approx 2s\)

TheoremNonnegativity of the survival probability#✓fully proved

The survival probability is non-negative.

theorem survivalProb_nonneg (s : ℝ) : 0 ≤ survivalProb s

Uses 4

Statement usesHaldane's survival probability of a mutant

Proof usesExtinction probability of a Galton–Watson process · Extinction probability is the least fixed point · Probability generating function

TheoremHaldane's approximation \(\pi(s) \approx 2s\)#✓fully proved

Haldane's approximation (Haldane 1927): π(s) / s → 2 as s → 0⁺.

theorem tendsto_survivalProb_div :
    Tendsto (fun s => survivalProb s / s) (𝓝[>] 0) (𝓝 2)

Uses 4

Statement usesHaldane's survival probability of a mutant

Proof usesHaldane's equation for the survival probability · Survival probability is less than one · Beneficial mutant survives with positive probability

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.