Λ-coalescents

DefinitionPitman's merger rate#✓fully proved

Pitman's merger rate λ_{b,k} = ∫ x ^ (k - 2) (1 - x) ^ (b - k) Λ(dx): while there are b blocks, the rate at which a given set of k of them merges into one block, for 2 ≤ k ≤ b (Pitman 1999, Theorem 1; Sagitov 1999). Powers are natural-number powers, so 0 ^ 0 = 1. Outside 2 ≤ k ≤ b no such merger exists, and the rate is defined to be 0.

def mergerRate [IsFiniteMeasure Λ] (b k : ℕ) : ℝ :=
  if 2 ≤ k ∧ k ≤ b then ∫ x, (x : ℝ) ^ (k - 2) * (1 - (x : ℝ)) ^ (b - k) ∂Λ else 0

Used by 18

Used byGenerator of the Λ-coalescent block-counting process · Uniqueness in Pitman's representation · Pitman's representation theorem, existence half · Λ-coalescent block-counting generator is a rate matrix · Pitman's consistency relation · Kingman's coalescent · Merger rates are bounded by the total mass of Λ · Nonnegativity of Λ-coalescent merger rates · Pitman's integral formula for merger rates when \(2 \le k \le b\) · Pair merger rate of a Λ-coalescent · Merger rates of the Bolthausen–Sznitman coalescent · Total merger rate of a Λ-coalescent · Total merger rate of Kingman's coalescent · The total merger rate in closed form · Monotonicity of the total merger rate · Nonnegativity of the total merger rate · Recursion for the total merger rate · Total merger rate of the Bolthausen–Sznitman coalescent

DefinitionTotal merger rate of a Λ-coalescent#✓fully proved

The total merger rate λ_b = ∑_{k=2}^b (b.choose k) λ_{b,k} while there are b blocks (Pitman 1999; Berestycki 2009, §3.1).

def totalMergerRate [IsFiniteMeasure Λ] (b : ℕ) : ℝ :=
  ∑ k ∈ Icc 2 b, (b.choose k : ℝ) * mergerRate Λ b k

Uses 1 · Used by 8

Statement usesPitman's merger rate

Used byGenerator of the Λ-coalescent block-counting process · Λ-coalescent block-counting generator is a rate matrix · Total merger rate of Kingman's coalescent · The total merger rate in closed form · Monotonicity of the total merger rate · Nonnegativity of the total merger rate · Recursion for the total merger rate · Total merger rate of the Bolthausen–Sznitman coalescent

DefinitionGenerator of the Λ-coalescent block-counting process#✓fully proved

The generator of the block-counting process of the Λ-coalescent on the states 0, …, n (state b means b blocks): from b blocks the process jumps to j < b blocks at rate (b.choose (b + 1 - j)) λ_{b, b + 1 - j} (a (b + 1 - j)-merger), and the diagonal is -λ_b. States 0 and 1 are absorbing (state 0 is never reached from b ≥ 1).

def blockCountingGenerator [IsFiniteMeasure Λ] (n : ℕ) :
    Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ := fun i j =>
  if i = j then -totalMergerRate Λ i
  else if (j : ℕ) < i then ((i : ℕ).choose (i + 1 - j) : ℝ) * mergerRate Λ i (i + 1 - j)
  else 0

Uses 2 · Used by 1

Statement usesPitman's merger rate · Total merger rate of a Λ-coalescent

Used byΛ-coalescent block-counting generator is a rate matrix

TheoremPitman's integral formula for merger rates when \(2 \le k \le b\)#✓fully proved

The merger rate inside its domain.

theorem mergerRate_of_le {b k : ℕ} (hk : 2 ≤ k) (hkb : k ≤ b) :
    mergerRate Λ b k = ∫ x, (x : ℝ) ^ (k - 2) * (1 - (x : ℝ)) ^ (b - k) ∂Λ

Uses 1 · Used by 5

Statement usesPitman's merger rate

Used byUniqueness in Pitman's representation · Pitman's consistency relation · Merger rates of the Bolthausen–Sznitman coalescent · The total merger rate in closed form · Recursion for the total merger rate

TheoremNonnegativity of Λ-coalescent merger rates#✓fully proved

Merger rates are nonnegative.

theorem mergerRate_nonneg (b k : ℕ) : 0 ≤ mergerRate Λ b k

Uses 1 · Used by 3

Statement usesPitman's merger rate

Used byΛ-coalescent block-counting generator is a rate matrix · Monotonicity of the total merger rate · Nonnegativity of the total merger rate

TheoremPair merger rate of a Λ-coalescent#✓fully proved

Two blocks merge at rate Λ [0, 1]; Λ is often normalized to a probability measure, so that this pair rate is 1 as in Kingman's coalescent.

theorem mergerRate_two_two : mergerRate Λ 2 2 = Λ.real Set.univ

Uses 1

Statement usesPitman's merger rate

TheoremNonnegativity of the total merger rate#✓fully proved

The total merger rate is nonnegative.

theorem totalMergerRate_nonneg (b : ℕ) : 0 ≤ totalMergerRate Λ b

Uses 3

Statement usesTotal merger rate of a Λ-coalescent

Proof usesPitman's merger rate · Nonnegativity of Λ-coalescent merger rates

TheoremΛ-coalescent block-counting generator is a rate matrix#✓fully proved

The block-counting generator is a rate matrix: its jump rates are nonnegative and each row sums to 0, since the jump rates out of b blocks add up to λ_b.

theorem isRateMatrix_blockCountingGenerator (n : ℕ) :
    ProbabilityTheory.IsRateMatrix (blockCountingGenerator Λ n)

Uses 5

Statement usesGenerator of the Λ-coalescent block-counting process · Rate matrix

Proof usesPitman's merger rate · Nonnegativity of Λ-coalescent merger rates · Total merger rate of a Λ-coalescent

TheoremMerger rates are bounded by the total mass of Λ#✓fully proved

A merger rate is at most the total mass of Λ.

theorem mergerRate_le_measure_univ (b k : ℕ) : mergerRate Λ b k ≤ Λ.real Set.univ

Uses 1

Statement usesPitman's merger rate

TheoremPitman's consistency relation#✓fully proved

Pitman's consistency relation λ_{b,k} = λ_{b+1,k} + λ_{b+1,k+1} for 2 ≤ k ≤ b (Pitman 1999; Berestycki 2009, §3.1): a given k-set of b blocks merges, with an extra block present, either without it or together with it.

theorem mergerRate_consistent {b k : ℕ} (hk : 2 ≤ k) (hkb : k ≤ b) :
    mergerRate Λ b k = mergerRate Λ (b + 1) k + mergerRate Λ (b + 1) (k + 1)

Uses 2

Statement usesPitman's merger rate

Proof usesPitman's integral formula for merger rates when \(2 \le k \le b\)

TheoremBinomial identity behind the total merger rate#✓fully proved

The polynomial identity behind the closed form of the total merger rate: x ^ 2 ∑_{k=2}^b (b.choose k) x ^ (k - 2) (1 - x) ^ (b - k) = 1 - (1 - x) ^ b - b x (1 - x) ^ (b - 1) for every real x and every b (binomial theorem).

theorem sq_mul_sum_choose_mul_pow (x : ℝ) (b : ℕ) :
    x ^ 2 * ∑ k ∈ Icc 2 b, (b.choose k : ℝ) * (x ^ (k - 2) * (1 - x) ^ (b - k)) =
      1 - (1 - x) ^ b - b * x * (1 - x) ^ (b - 1)

Used by 2

Used byThe total merger rate in closed form · Recursion for the total merger rate

TheoremThe total merger rate in closed form#✓fully proved

The total merger rate in closed form (Berestycki 2009, §3.1): λ_b = (b.choose 2) Λ {0} + ∫_{(0,1]} (1 - (1 - x) ^ b - b x (1 - x) ^ (b - 1)) / x ^ 2 Λ(dx). The atom at 0 (the Kingman part) is split off, so no division by 0 occurs.

theorem totalMergerRate_eq (b : ℕ) :
    totalMergerRate Λ b = (b.choose 2 : ℝ) * Λ.real {0} +
      ∫ x in ({0}ᶜ : Set I),
        (1 - (1 - (x : ℝ)) ^ b - b * (x : ℝ) * (1 - (x : ℝ)) ^ (b - 1)) / (x : ℝ) ^ 2 ∂Λ

Uses 4

Statement usesTotal merger rate of a Λ-coalescent

Proof usesPitman's merger rate · Pitman's integral formula for merger rates when \(2 \le k \le b\) · Binomial identity behind the total merger rate

TheoremRecursion for the total merger rate#✓fully proved

Adding a block raises the total merger rate by b λ_{b+1,2}: λ_{b+1} = λ_b + b λ_{b+1,2}. The new events are exactly the binary mergers of the new block with one of the b old ones (a consequence of the consistency relation).

theorem totalMergerRate_succ (b : ℕ) :
    totalMergerRate Λ (b + 1) = totalMergerRate Λ b + b * mergerRate Λ (b + 1) 2

Uses 4 · Used by 1

Statement usesPitman's merger rate · Total merger rate of a Λ-coalescent

Proof usesPitman's integral formula for merger rates when \(2 \le k \le b\) · Binomial identity behind the total merger rate

Used byMonotonicity of the total merger rate

TheoremMonotonicity of the total merger rate#✓fully proved

The total merger rate λ_b is nondecreasing in the number of blocks b.

theorem totalMergerRate_mono : Monotone (totalMergerRate Λ)

Uses 4

Statement usesTotal merger rate of a Λ-coalescent

Proof usesPitman's merger rate · Nonnegativity of Λ-coalescent merger rates · Recursion for the total merger rate

TheoremUniqueness in Pitman's representation#✓fully proved

A finite measure on [0, 1] is determined by its merger rates; indeed by the rates λ_{k,k} = ∫ x ^ (k - 2) Λ(dx) of complete mergers, which are its moments (Pitman 1999, Theorem 1).

theorem eq_of_mergerRate_eq (Λ' : Measure I) [IsFiniteMeasure Λ']
    (h : ∀ k, 2 ≤ k → mergerRate Λ k k = mergerRate Λ' k k) : Λ = Λ'

Uses 2

Statement usesPitman's merger rate

Proof usesPitman's integral formula for merger rates when \(2 \le k \le b\)

TheoremKingman's coalescent#✓fully proved

Kingman's coalescent is the Λ-coalescent with Λ = δ₀: only binary mergers occur, each pair merging at rate 1 (Pitman 1999; Berestycki 2009, §3.1).

theorem mergerRate_dirac_zero (b k : ℕ) :
    mergerRate (Measure.dirac 0) b k = if k = 2 ∧ 2 ≤ b then 1 else 0

Uses 1 · Used by 1

Statement usesPitman's merger rate

Used byTotal merger rate of Kingman's coalescent

TheoremTotal merger rate of Kingman's coalescent#✓fully proved

For Kingman's coalescent the total merger rate is the number of pairs, λ_b = b.choose 2.

theorem totalMergerRate_dirac_zero (b : ℕ) :
    totalMergerRate (Measure.dirac 0) b = b.choose 2

Uses 3

Statement usesTotal merger rate of a Λ-coalescent

Proof usesPitman's merger rate · Kingman's coalescent

TheoremMerger rates of the Bolthausen–Sznitman coalescent#✓fully proved

The Bolthausen–Sznitman coalescent (Λ = Lebesgue measure on [0, 1]) has merger rates given by the Beta integral λ_{b,k} = (k - 2)! (b - k)! / (b - 1)! for 2 ≤ k ≤ b (Bolthausen–Sznitman 1998; Pitman 1999; Berestycki 2009, §3.1).

theorem mergerRate_volume {b k : ℕ} (hk : 2 ≤ k) (hkb : k ≤ b) :
    mergerRate volume b k =
      ((k - 2).factorial * (b - k).factorial : ℝ) / (b - 1).factorial

Uses 2 · Used by 1

Statement usesPitman's merger rate

Proof usesPitman's integral formula for merger rates when \(2 \le k \le b\)

Used byTotal merger rate of the Bolthausen–Sznitman coalescent

TheoremTotal merger rate of the Bolthausen–Sznitman coalescent#✓fully proved

For the Bolthausen–Sznitman coalescent the total merger rate is λ_b = b - 1 (b ≥ 1).

theorem totalMergerRate_volume {b : ℕ} (hb : 1 ≤ b) :
    totalMergerRate volume b = b - 1

Uses 4

Statement usesTotal merger rate of a Λ-coalescent

Proof usesPitman's merger rate · Merger rates of the Bolthausen–Sznitman coalescent · Sum of reciprocals of binomial coefficients \(\binom{k}{2}\)

TheoremPitman's representation theorem, existence half#●ready to prove

Pitman's representation theorem, existence half (Pitman 1999, Theorem 1): every consistent family of nonnegative merger rates r b k, 2 ≤ k ≤ b, is the family of merger rates λ_{b,k} of some finite measure Λ on [0, 1]. (Uniqueness of Λ is LambdaCoalescent.eq_of_mergerRate_eq.)

theorem_wanted exists_measure_of_consistent (r : ℕ → ℕ → ℝ)
    (hnonneg : ∀ b k, 2 ≤ k → k ≤ b → 0 ≤ r b k)
    (hcons : ∀ b k, 2 ≤ k → k ≤ b → r b k = r (b + 1) k + r (b + 1) (k + 1)) :
    ∃ (Λ : Measure I) (_ : IsFiniteMeasure Λ), ∀ b k, 2 ≤ k → k ≤ b → r b k = mergerRate Λ b k

Sources

• Pitman (1999), Theorem 1; Hausdorff (1921).

Uses 1

Statement usesPitman's merger rate

19 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.