Luria–Delbrück distribution

DefinitionLea–Coulson clone-size law#✓fully proved

The Lea–Coulson clone-size law P(size = j) = 1 / (j (j + 1)) for j ≥ 1 (P(size = 0) = 0).

noncomputable def cloneProb (j : ℕ) : ℝ :=
  if j = 0 then 0 else 1 / ((j : ℝ) * (j + 1))
Used by 9
Used byThe clone-size law sums to one · Clone-size generating function · The Luria–Delbrück probabilities sum to one · Lea–Coulson generating function · Clone-size law from the founding-time density · Luria–Delbrück distribution · Nonnegativity of Luria–Delbrück probabilities · Ma–Sandri–Sarkar recursion · p₀

DefinitionConvolution power of a sequence on the naturals#✓fully proved

The k-fold convolution power of a sequence on ℕ: p^{*0} = δ₀ and p^{*(k+1)}(n) = ∑_{i ≤ n} p(i) p^{*k}(n - i).

noncomputable def convPow (p : ℕ → ℝ) : ℕ → ℕ → ℝ
  | 0, n => if n = 0 then 1 else 0
  | k + 1, n => ∑ i ∈ range (n + 1), p i * convPow p k (n - i)
Used by 6
Used byThe Luria–Delbrück probabilities sum to one · Lea–Coulson generating function · Luria–Delbrück distribution · Nonnegativity of Luria–Delbrück probabilities · Ma–Sandri–Sarkar recursion · p₀

DefinitionLuria–Delbrück distribution#✓fully proved

The Luria–Delbrück probability of n mutants with expected mutation number m: the compound-Poisson law ∑_k e^{-m} m^k / k! · cloneProb^{*k}(n). Since clones have size at least 1, only k ≤ n contribute.

noncomputable def ldPmf (m : ℝ) (n : ℕ) : ℝ :=
  ∑ k ∈ range (n + 1), exp (-m) * m ^ k / k.factorial * convPow cloneProb k n
Uses 2 · Used by 6
Statement usesLea–Coulson clone-size law · Convolution power of a sequence on the naturals
Used byThe Luria–Delbrück probabilities sum to one · Lea–Coulson generating function · Nonnegativity of Luria–Delbrück probabilities · Ma–Sandri–Sarkar recursion · p₀ · The p₀ method

DefinitionClosed form of the clone-size generating function#✓fully proved

The clone-size generating function h(z) = 1 + (1 / z - 1) log (1 - z).

noncomputable def clonePgf (z : ℝ) : ℝ :=
  1 + (1 / z - 1) * log (1 - z)
Used by 2
Used byClone-size generating function · Lea–Coulson generating function

TheoremClone-size law from the founding-time density#✓fully proved

A clone founded τ before the end has geometric size e^{-τ} (1 - e^{-τ})^{j-1}; mixing over the founding-time density e^{-τ} on (0, ∞) gives 1 / (j (j + 1)) for j ≥ 1.

theorem integral_cloneSize {j : ℕ} (hj : 1 ≤ j) :
    ∫ τ in Ioi (0 : ℝ), exp (-τ) * (exp (-τ) * (1 - exp (-τ)) ^ (j - 1)) = cloneProb j
Uses 1
Statement usesLea–Coulson clone-size law

TheoremThe clone-size law sums to one#✓fully proved

The clone-size law sums to 1.

theorem hasSum_cloneProb : HasSum cloneProb 1
Uses 1 · Used by 1
Statement usesLea–Coulson clone-size law
Used byThe Luria–Delbrück probabilities sum to one

TheoremClone-size generating function#✓fully proved

For 0 < z < 1, ∑ⱼ zʲ / (j (j + 1)) = 1 + (1 / z - 1) log (1 - z).

theorem hasSum_cloneProb_mul_pow {z : ℝ} (hz0 : 0 < z) (hz1 : z < 1) :
    HasSum (fun j => cloneProb j * z ^ j) (clonePgf z)
Uses 2 · Used by 1
Statement usesClosed form of the clone-size generating function · Lea–Coulson clone-size law
Used byLea–Coulson generating function

Theoremp₀#✓fully proved

The probability of no mutants is e^{-m}.

theorem ldPmf_zero (m : ℝ) : ldPmf m 0 = exp (-m)
Uses 3 · Used by 1
Statement usesLuria–Delbrück distribution
Proof usesLea–Coulson clone-size law · Convolution power of a sequence on the naturals
Used byThe p₀ method

TheoremThe p₀ method#✓fully proved

The p₀ method (Luria–Delbrück 1943): the expected number of mutations is recovered from the proportion of cultures with no mutants, m = -log p₀.

theorem p0_method (m : ℝ) : m = -log (ldPmf m 0)
Uses 2
Statement usesLuria–Delbrück distribution
Proof usesp₀

TheoremNonnegativity of Luria–Delbrück probabilities#✓fully proved

The Luria–Delbrück probabilities are nonnegative for m ≥ 0.

theorem ldPmf_nonneg {m : ℝ} (hm : 0 ≤ m) (n : ℕ) : 0 ≤ ldPmf m n
Uses 3
Statement usesLuria–Delbrück distribution
Proof usesLea–Coulson clone-size law · Convolution power of a sequence on the naturals

TheoremThe Luria–Delbrück probabilities sum to one#✓fully proved

The Luria–Delbrück probabilities sum to 1 (for m ≥ 0).

theorem hasSum_ldPmf {m : ℝ} (hm : 0 ≤ m) : HasSum (ldPmf m) 1
Uses 4
Statement usesLuria–Delbrück distribution
Proof usesLea–Coulson clone-size law · Convolution power of a sequence on the naturals · The clone-size law sums to one

TheoremLea–Coulson generating function#✓fully proved

For m ≥ 0 and 0 < z < 1, ∑ₙ pₙ zⁿ = exp (m (h(z) - 1)) = exp (m (1 / z - 1) log (1 - z)).

theorem hasSum_ldPmf_mul_pow {m : ℝ} (hm : 0 ≤ m) {z : ℝ} (hz0 : 0 < z) (hz1 : z < 1) :
    HasSum (fun n => ldPmf m n * z ^ n) (exp (m * ((1 / z - 1) * log (1 - z))))
Uses 5
Statement usesLuria–Delbrück distribution
Proof usesClosed form of the clone-size generating function · Lea–Coulson clone-size law · Convolution power of a sequence on the naturals · Clone-size generating function

TheoremPower form of the Lea–Coulson generating function#✓fully proved

The Lea–Coulson generating function in power form: exp (m (1 / z - 1) log (1 - z)) = (1 - z)^{m (1 - z) / z} for z < 1, z ≠ 0.

theorem exp_leaCoulson_eq_rpow (m : ℝ) {z : ℝ} (hz0 : z ≠ 0) (hz1 : z < 1) :
    exp (m * ((1 / z - 1) * log (1 - z))) = (1 - z) ^ (m * (1 - z) / z)

TheoremMa–Sandri–Sarkar recursion#✓fully proved

For n ≥ 1, pₙ = (m / n) ∑_{i < n} pᵢ / (n - i + 1) (all real m).

theorem ldPmf_recursion (m : ℝ) {n : ℕ} (hn : 1 ≤ n) :
    ldPmf m n = m / n * ∑ i ∈ range n, ldPmf m i / ((n : ℝ) - i + 1)
Uses 3
Statement usesLuria–Delbrück distribution
Proof usesLea–Coulson clone-size law · Convolution power of a sequence on the naturals
14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.