Site frequency spectrum under variable population size

DefinitionGriffiths–Tavaré kernel#✓fully proved

The Griffiths–Tavaré kernel k C(n-i-1, k-2) / C(n-1, k-1): the expected number of branches subtending exactly i of the n sample copies while k lineages remain (SiteFrequencySpectrum.joinStep_iterate_count). Meaningful for 1 ≤ i < n, 2 ≤ k ≤ n; outside that range the natural-number subtractions give junk values.

def sfsKernel (n i k : ℕ) : ℝ :=
  k * ((n - i - 1).choose (k - 2) : ℝ) / ((n - 1).choose (k - 1) : ℝ)

Used by 6

Used byThe expected SFS determines the mean holding times · Expected SFS under a variable population size · Positivity of the Griffiths–Tavaré kernel on the diagonal · Griffiths–Tavaré kernel vanishes beyond the diagonal · Expected site frequency spectrum under variable population size · Variable-size spectrum reduces to Fu's \(\theta/i\) at constant size

DefinitionExpected site frequency spectrum under variable population size#✓fully proved

The expected SFS entry (θ / 2) ∑_{k=2}^{n} sfsKernel n i k · t k of a sample of size n whose mean holding times are t k = E T_k (Griffiths & Tavaré 1998, Polanski & Kimmel 2003).

def variableSFS (θ : ℝ) (n : ℕ) (t : ℕ → ℝ) (i : ℕ) : ℝ :=
  θ / 2 * ∑ k ∈ Icc 2 n, sfsKernel n i k * t k

Uses 1 · Used by 3

Statement usesGriffiths–Tavaré kernel

Used byThe expected SFS determines the mean holding times · Expected SFS under a variable population size · Variable-size spectrum reduces to Fu's \(\theta/i\) at constant size

TheoremExpected SFS under a variable population size#✓fully proved

Expected SFS under a variable population size (Griffiths & Tavaré 1998; Polanski & Kimmel 2003). Let the genealogy of a sample of n copies consist of holding times T k (integrable for 2 ≤ k ≤ n, otherwise arbitrary) and an independent block-size history τ with the random-joining law. If, given the genealogy, the count ξ i is integrable with conditional mean (θ / 2) L_i, then E ξ_i = (θ / 2) ∑_k k C(n-i-1,k-2)/C(n-1,k-1) E T_k for 1 ≤ i ≤ n - 1. Independence of the holding times and the topology holds for the time-changed Kingman coalescent of any deterministic population-size history (a standard property of that model; here it is a hypothesis).

theorem integral_sfs_of_indep {μ : Measure Ω} [IsProbabilityMeasure μ] {n : ℕ}
    {T : ℕ → Ω → ℝ} (hT : ∀ k, Measurable (T k)) (hT_int : ∀ k ∈ Icc 2 n, Integrable (T k) μ)
    {τ : Ω → List (List ℕ)} (hτ : MeasurableSpace.comap τ ⊤ ≤ mΩ)
    (hτ_law : ∀ ps, μ.real (τ ⁻¹' {ps}) =
      randomJoining (n - 1) (List.replicate n 1) ps)
    (h_indep : Indep (MeasurableSpace.comap τ ⊤)
      (MeasurableSpace.comap (fun ω k => T k ω) MeasurableSpace.pi) μ)
    {θ : ℝ} {ξ : ℕ → Ω → ℝ} (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i, μ[ξ i | MeasurableSpace.comap τ ⊤ ⊔
        MeasurableSpace.comap (fun ω k => T k ω) MeasurableSpace.pi] =ᵐ[μ]
      fun ω => θ / 2 * sfsLength n i (τ ω) (fun k => T k ω))
    {i : ℕ} (hi : 1 ≤ i) (hin : i < n) :
    μ[ξ i] = variableSFS θ n (fun k => μ[T k]) i

Uses 7

Statement usesRandom-joining law on block-size lists · Total branch length subtending i sample copies · Expected site frequency spectrum under variable population size

Proof usesRandom joining has finite support and iterates the join step · Transition operator of random joining · Expected number of blocks of size i · Griffiths–Tavaré kernel

TheoremVariable-size spectrum reduces to Fu's \(\theta/i\) at constant size#✓fully proved

With the constant-size means E T_k = 1 / C(k,2), the variable-size SFS is Fu's θ / i.

theorem variableSFS_inv_choose_two (θ : ℝ) {n i : ℕ} (hi : 1 ≤ i) (hin : i < n) :
    variableSFS θ n (fun k => ((k.choose 2 : ℕ) : ℝ)⁻¹) i = θ / i

Uses 3

Statement usesExpected site frequency spectrum under variable population size

Proof usesExpected block counts weighted by coalescence times sum to \(2/i\) · Griffiths–Tavaré kernel

TheoremGriffiths–Tavaré kernel vanishes beyond the diagonal#✓fully proved

The kernel row i vanishes beyond k = n - i + 1: a branch subtending i copies cannot exist while more than n - i + 1 lineages remain.

theorem sfsKernel_eq_zero_of_lt {n i k : ℕ} (hin : i < n) (hk : n - i + 1 < k) :
    sfsKernel n i k = 0

Uses 1 · Used by 1

Statement usesGriffiths–Tavaré kernel

Used byThe expected SFS determines the mean holding times

TheoremPositivity of the Griffiths–Tavaré kernel on the diagonal#✓fully proved

The kernel entry at k = n - i + 1 is (n - i + 1) / C(n-1, i-1) > 0.

theorem sfsKernel_diag_pos {n i : ℕ} (hi : 1 ≤ i) (hin : i < n) :
    0 < sfsKernel n i (n - i + 1)

Uses 1 · Used by 1

Statement usesGriffiths–Tavaré kernel

Used byThe expected SFS determines the mean holding times

TheoremThe expected SFS determines the mean holding times#✓fully proved

If two vectors of mean holding times give the same expected SFS for some θ ≠ 0, they agree at every k = 2, …, n. This is a direct consequence of sfsKernel_eq_zero_of_lt and sfsKernel_diag_pos (the kernel is triangular with nonzero diagonal); it is recorded here as an observation, not as a cited theorem.

theorem eq_of_variableSFS_eq {θ : ℝ} (hθ : θ ≠ 0) {n : ℕ} {t t' : ℕ → ℝ}
    (h : ∀ i ∈ Ico 1 n, variableSFS θ n t i = variableSFS θ n t' i) :
    ∀ k ∈ Icc 2 n, t k = t' k

Uses 4

Statement usesExpected site frequency spectrum under variable population size

Proof usesGriffiths–Tavaré kernel · Positivity of the Griffiths–Tavaré kernel on the diagonal · Griffiths–Tavaré kernel vanishes beyond the diagonal

DefinitionAchaz's weighted estimator of \(\theta\)#✓fully proved

Achaz's weighted estimator θ_ω = ∑_{i=1}^{n-1} ω_i i ξ_i (Achaz 2009, with the weights already normalized).

def thetaWeighted (n : ℕ) (w : ℕ → ℝ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ :=
  fun ω => ∑ i ∈ Ico 1 n, w i * i * ξ i ω

Used by 6

Used byFay and Wu's H has mean zero at constant size · Numerator of Fu and Li's F has mean zero at constant size · Achaz's unbiasedness · Achaz's estimator is unbiased under Kingman's coalescent · Fay and Wu's \(\theta_H\) · Tajima's \(\theta_\pi\) in site frequency spectrum form

DefinitionTajima's \(\theta_\pi\) in site frequency spectrum form#✓fully proved

Tajima's θ_π in its SFS form ∑_i i (n - i) ξ_i / C(n,2) (weights (n - i) / C(n,2)).

def thetaPi (n : ℕ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ :=
  thetaWeighted n (fun i => ((n : ℝ) - i) / (n.choose 2 : ℝ)) ξ

Uses 1 · Used by 4

Statement usesAchaz's weighted estimator of \(\theta\)

Used byFay and Wu's H statistic · Numerator of Fu and Li's F · Fay and Wu's H has mean zero at constant size · Numerator of Fu and Li's F has mean zero at constant size

DefinitionFay and Wu's \(\theta_H\)#✓fully proved

Fay & Wu's θ_H = ∑_i i² ξ_i / C(n,2) (weights i / C(n,2)).

def thetaH (n : ℕ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ :=
  thetaWeighted n (fun i => (i : ℝ) / (n.choose 2 : ℝ)) ξ

Uses 1 · Used by 2

Statement usesAchaz's weighted estimator of \(\theta\)

Used byFay and Wu's H statistic · Fay and Wu's H has mean zero at constant size

DefinitionFay and Wu's H statistic#✓fully proved

Fay & Wu's H = θ_π - θ_H (Fay & Wu 2000).

def fayWuH (n : ℕ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ := fun ω => thetaPi n ξ ω - thetaH n ξ ω

Uses 2 · Used by 1

Statement usesFay and Wu's \(\theta_H\) · Tajima's \(\theta_\pi\) in site frequency spectrum form

Used byFay and Wu's H has mean zero at constant size

DefinitionNumerator of Fu and Li's D#✓fully proved

The numerator S - a₁ ξ₁ of Fu & Li's D with an outgroup, where S = ∑_i ξ_i and the external-branch mutations are the derived singletons ξ₁ (Fu & Li 1993).

def fuLiDNumerator (n : ℕ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ :=
  fun ω => ∑ i ∈ Ico 1 n, ξ i ω - tajimaA1 n * ξ 1 ω

Uses 1 · Used by 1

Statement usesTajima's constant \(a_1\)

Used byNumerator of Fu and Li's D has mean zero at constant size

DefinitionNumerator of Fu and Li's F#✓fully proved

The numerator θ_π - ξ₁ of Fu & Li's F with an outgroup (Fu & Li 1993), with θ_π in its SFS form.

def fuLiFNumerator (n : ℕ) (ξ : ℕ → Ω → ℝ) : Ω → ℝ := fun ω => thetaPi n ξ ω - ξ 1 ω

Uses 1 · Used by 1

Statement usesTajima's \(\theta_\pi\) in site frequency spectrum form

Used byNumerator of Fu and Li's F has mean zero at constant size

TheoremAchaz's unbiasedness#✓fully proved

Achaz's unbiasedness (Achaz 2009): if E ξ_i = θ / i for 1 ≤ i ≤ n - 1 (the constant-size spectrum, SiteFrequencySpectrum.integral_sfs), every weighted estimator with ∑_i ω_i = 1 has mean θ.

theorem integral_thetaWeighted (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i ∈ Ico 1 n, μ[ξ i] = θ / i) {w : ℕ → ℝ} (hw : ∑ i ∈ Ico 1 n, w i = 1) :
    μ[thetaWeighted n w ξ] = θ

Uses 1 · Used by 3

Statement usesAchaz's weighted estimator of \(\theta\)

Used byFay and Wu's H has mean zero at constant size · Numerator of Fu and Li's F has mean zero at constant size · Achaz's estimator is unbiased under Kingman's coalescent

TheoremFay and Wu's H has mean zero at constant size#✓fully proved

Fay & Wu's H has mean zero under the constant-size spectrum (n ≥ 2).

theorem integral_fayWuH (hn : 2 ≤ n) (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i ∈ Ico 1 n, μ[ξ i] = θ / i) : μ[fayWuH n ξ] = 0

Uses 5

Statement usesFay and Wu's H statistic

Proof usesAchaz's unbiasedness · Fay and Wu's \(\theta_H\) · Tajima's \(\theta_\pi\) in site frequency spectrum form · Achaz's weighted estimator of \(\theta\)

TheoremNumerator of Fu and Li's D has mean zero at constant size#✓fully proved

The numerator of Fu & Li's D has mean zero under the constant-size spectrum (n ≥ 2).

theorem integral_fuLiDNumerator (hn : 2 ≤ n) (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i ∈ Ico 1 n, μ[ξ i] = θ / i) : μ[fuLiDNumerator n ξ] = 0

Uses 2

Statement usesNumerator of Fu and Li's D

Proof usesTajima's constant \(a_1\)

TheoremNumerator of Fu and Li's F has mean zero at constant size#✓fully proved

The numerator of Fu & Li's F has mean zero under the constant-size spectrum (n ≥ 2).

theorem integral_fuLiFNumerator (hn : 2 ≤ n) (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i ∈ Ico 1 n, μ[ξ i] = θ / i) : μ[fuLiFNumerator n ξ] = 0

Uses 4

Statement usesNumerator of Fu and Li's F

Proof usesAchaz's unbiasedness · Tajima's \(\theta_\pi\) in site frequency spectrum form · Achaz's weighted estimator of \(\theta\)

TheoremAchaz's estimator is unbiased under Kingman's coalescent#✓fully proved

Achaz's unbiasedness under Kingman's coalescent, with the hypotheses of SiteFrequencySpectrum.integral_sfs.

theorem integral_thetaWeighted_kingman [IsProbabilityMeasure μ]
    (K : KingmanTimes μ n) (hT : ∀ k, Measurable (K.T k))
    {τ : Ω → List (List ℕ)} (hτ : MeasurableSpace.comap τ ⊤ ≤ mΩ)
    (hτ_law : ∀ ps, μ.real (τ ⁻¹' {ps}) =
      randomJoining (n - 1) (List.replicate n 1) ps)
    (h_indep : Indep (MeasurableSpace.comap τ ⊤)
      (MeasurableSpace.comap (fun ω k => K.T k ω) MeasurableSpace.pi) μ)
    (hξ_int : ∀ i, Integrable (ξ i) μ)
    (hξ : ∀ i, μ[ξ i | MeasurableSpace.comap τ ⊤ ⊔
        MeasurableSpace.comap (fun ω k => K.T k ω) MeasurableSpace.pi] =ᵐ[μ]
      fun ω => θ / 2 * sfsLength n i (τ ω) (fun k => K.T k ω))
    {w : ℕ → ℝ} (hw : ∑ i ∈ Ico 1 n, w i = 1) :
    μ[thetaWeighted n w ξ] = θ

Uses 6

Statement usesHolding times of Kingman's coalescent · Random-joining law on block-size lists · Total branch length subtending i sample copies · Achaz's weighted estimator of \(\theta\)

Proof usesExpected site frequency spectrum · Achaz's unbiasedness

DefinitionCumulative coalescence intensity#✓fully proved

The cumulative coalescence intensity R(s) = ∫_0^s 1/η of a relative population-size function η (pairs coalesce at rate 1/η(s) at time s before the present). Meaningful for positive η with 1/η locally integrable.

def cumRate (η : ℝ → ℝ) (s : ℝ) : ℝ := ∫ r in (0 : ℝ)..s, (η r)⁻¹

Used by 11

Used byClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Cumulative rate is affine on each piece · Coalescent-time breakpoints are strictly increasing · Cumulative rate is strictly increasing · Dual history in coalescent time · Tightness of n ≥ 2K · Expected time to the first coalescence · First-coalescence times depend only on sizes at nonnegative times · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability

DefinitionExpected time to the first coalescence#✓fully proved

The expected time to the first coalescence among m lineages, c_m = ∫_0^∞ exp(-C(m,2) R(s)) ds, in a population of relative size η (Bhaskar & Song's E[T_{m,m}]). When the integrand is not integrable (for example η ≡ 0), this is Lean's junk value 0; for piecewise-constant histories it is integrable (choose_two_mul_firstCoalMean).

def firstCoalMean (η : ℝ → ℝ) (m : ℕ) : ℝ :=
  ∫ s in Set.Ioi 0, Real.exp (-((m.choose 2 : ℕ) : ℝ) * cumRate η s)

Uses 1 · Used by 7

Statement usesCumulative coalescence intensity

Used byClosed form of the first-coalescence times · Non-identifiability of general histories · Non-identifiability from a bounded sample size · Tightness of n ≥ 2K · Distinct two-piece histories with equal first-coalescence times · First-coalescence times depend only on sizes at nonnegative times · Bhaskar–Song identifiability

StructurePiecewise-constant population-size history#✓fully proved

A piecewise-constant population-size history with K pieces: piece j < K starts at time start j (backward from the present, start 0 = 0, strictly increasing) and has relative size size j > 0; the last piece extends to infinity. Adjacent pieces may have equal sizes, so this also covers histories with fewer than K distinct pieces. Values at indices j ≥ K are unused. The case K = 0 is degenerate (its size function is 0); the theorems about c_m assume 0 < K where it matters.

structure PiecewiseHistory (K : ℕ) where
  /-- The relative size on piece `j`. -/
  size : ℕ → ℝ
  /-- The start time of piece `j`. -/
  start : ℕ → ℝ
  /-- Every piece has a positive size. -/
  size_pos : ∀ j < K, 0 < size j
  /-- The first piece starts at the present. -/
  start_zero : start 0 = 0
  /-- The pieces start at strictly increasing times. -/
  start_lt : ∀ j, j + 1 < K → start j < start (j + 1)

Used by 20

Used byClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Cumulative rate is affine on each piece · Coalescent-time breakpoints are strictly increasing · Cumulative rate is strictly increasing · Dual history in coalescent time · Size function lies between the extreme piece sizes · Non-identifiability from a bounded sample size · Tightness of n ≥ 2K · Distinct two-piece histories with equal first-coalescence times · Every nonnegative time lies in some piece · Size function is locally constant to the right · Measurability of the piecewise size function · Size function of a piecewise-constant history · Size function on a piece equals the piece size · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability · Positivity of the piecewise size function · Monotonicity of piece start times · Nonnegativity of piece start times

DefinitionSize function of a piecewise-constant history#✓fully proved

The population-size function of a piecewise-constant history: at time s ≥ 0 it is the size of the piece j with start j ≤ s < start (j + 1) (the last piece has no end). Equal to 0 for s < 0 (junk; only s ≥ 0 is meaningful).

def sizeFn (h : PiecewiseHistory K) (s : ℝ) : ℝ :=
  ∑ j ∈ range K, if h.start j ≤ s ∧ (j + 1 < K → s < h.start (j + 1)) then h.size j else 0

Uses 1 · Used by 16

Statement usesPiecewise-constant population-size history

Used byClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Cumulative rate is affine on each piece · Coalescent-time breakpoints are strictly increasing · Cumulative rate is strictly increasing · Dual history in coalescent time · Size function lies between the extreme piece sizes · Non-identifiability from a bounded sample size · Tightness of n ≥ 2K · Distinct two-piece histories with equal first-coalescence times · Size function is locally constant to the right · Measurability of the piecewise size function · Size function on a piece equals the piece size · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability · Positivity of the piecewise size function

TheoremMonotonicity of piece start times#✓fully proved

The start times are monotone on the pieces.

theorem start_mono (h : PiecewiseHistory K) {i j : ℕ} (hij : i ≤ j) (hj : j < K) :
    h.start i ≤ h.start j

Uses 1 · Used by 3

Statement usesPiecewise-constant population-size history

Used bySize function on a piece equals the piece size · Bhaskar–Song identifiability · Nonnegativity of piece start times

TheoremNonnegativity of piece start times#✓fully proved

Every piece starts at a nonnegative time.

theorem start_nonneg (h : PiecewiseHistory K) {j : ℕ} (hj : j < K) : 0 ≤ h.start j

Uses 2 · Used by 3

Statement usesPiecewise-constant population-size history

Proof usesMonotonicity of piece start times

Used byClosed form of the first-coalescence times · Tightness of n ≥ 2K · Bhaskar–Song identifiability

TheoremSize function on a piece equals the piece size#✓fully proved

On piece j the size function equals size j.

theorem sizeFn_eq (h : PiecewiseHistory K) {j : ℕ} {s : ℝ} (hj : j < K) (hs : h.start j ≤ s)
    (hs' : j + 1 < K → s < h.start (j + 1)) : h.sizeFn s = h.size j

Uses 3 · Used by 7

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history

Proof usesMonotonicity of piece start times

Used byCumulative rate is affine on each piece · Size function lies between the extreme piece sizes · Tightness of n ≥ 2K · Size function is locally constant to the right · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability · Positivity of the piecewise size function

TheoremCumulative rate is affine on each piece#✓fully proved

On piece j (including its right end), 1 / sizeFn is integrable on [0, s] and the cumulative rate is affine: R(s) = R(start j) + (s - start j) / size j.

theorem cumRate_piece (h : PiecewiseHistory K) :
    ∀ j < K, ∀ s, h.start j ≤ s → (j + 1 < K → s ≤ h.start (j + 1)) →
      IntervalIntegrable (fun r => (h.sizeFn r)⁻¹) volume 0 s ∧
      cumRate h.sizeFn s = cumRate h.sizeFn (h.start j) + (s - h.start j) / h.size j

Uses 4 · Used by 6

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Cumulative coalescence intensity

Proof usesSize function on a piece equals the piece size

Used byClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Coalescent-time breakpoints are strictly increasing · Cumulative rate is strictly increasing · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability

TheoremClosed form of the first-coalescence times#✓fully proved

For a history with K ≥ 1 pieces and m ≥ 2, writing a = C(m,2) and R = cumRate h.sizeFn, a c_m = size 0 + ∑_{j=1}^{K-1} (size j - size (j-1)) exp(-a R(start j)). In particular the integral defining c_m converges.

theorem choose_two_mul_firstCoalMean (h : PiecewiseHistory K) (hK : 0 < K) {m : ℕ}
    (hm : 2 ≤ m) :
    ((m.choose 2 : ℕ) : ℝ) * firstCoalMean h.sizeFn m =
      h.size 0 + ∑ j ∈ Ico 1 K, (h.size j - h.size (j - 1)) *
        Real.exp (-((m.choose 2 : ℕ) : ℝ) * cumRate h.sizeFn (h.start j))

Uses 6 · Used by 2

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Cumulative coalescence intensity · Expected time to the first coalescence

Proof usesCumulative rate is affine on each piece · Nonnegativity of piece start times

Used byTightness of n ≥ 2K · Bhaskar–Song identifiability

TheoremEvery nonnegative time lies in some piece#✓fully proved

Every time s ≥ 0 lies in some piece.

theorem exists_piece (h : PiecewiseHistory K) (hK : 0 < K) {s : ℝ} (hs : 0 ≤ s) :
    ∃ j < K, h.start j ≤ s ∧ (j + 1 < K → s < h.start (j + 1))

Uses 1 · Used by 7

Statement usesPiecewise-constant population-size history

Used byDual cumulative rate inverts the cumulative rate · Cumulative rate is strictly increasing · Size function lies between the extreme piece sizes · Size function is locally constant to the right · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability · Positivity of the piecewise size function

TheoremPositivity of the piecewise size function#✓fully proved

The size function is positive on [0, ∞).

theorem sizeFn_pos (h : PiecewiseHistory K) (hK : 0 < K) {s : ℝ} (hs : 0 ≤ s) :
    0 < h.sizeFn s

Uses 4 · Used by 1

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history

Proof usesEvery nonnegative time lies in some piece · Size function on a piece equals the piece size

Used byCumulative rate is strictly increasing

TheoremCoalescent-time breakpoints are strictly increasing#✓fully proved

The coalescent-time breakpoints R(start j) are strictly increasing.

theorem cumRate_start_lt (h : PiecewiseHistory K) {j : ℕ} (hj : j + 1 < K) :
    cumRate h.sizeFn (h.start j) < cumRate h.sizeFn (h.start (j + 1))

Uses 4 · Used by 3

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Cumulative coalescence intensity

Proof usesCumulative rate is affine on each piece

Used byDual cumulative rate inverts the cumulative rate · Dual history in coalescent time · Tightness of n ≥ 2K

DefinitionDual history in coalescent time#✓fully proved

The dual history in coalescent time: piece j starts at R(start j) and has size 1 / size j.

def dual (h : PiecewiseHistory K) : PiecewiseHistory K where
  size j := (h.size j)⁻¹
  start j := cumRate h.sizeFn (h.start j)
  size_pos j hj := inv_pos.2 (h.size_pos j hj)
  start_zero := by simp [h.start_zero, cumRate]
  start_lt j hj := h.cumRate_start_lt hj

Uses 4 · Used by 4

Statement usesPiecewise-constant population-size history · Coalescent-time breakpoints are strictly increasing · Size function of a piecewise-constant history · Cumulative coalescence intensity

Used byDual cumulative rate inverts the cumulative rate · Tightness of n ≥ 2K · Size function is the inverse of the dual size in coalescent time · Bhaskar–Song identifiability

TheoremSize function is the inverse of the dual size in coalescent time#✓fully proved

The size at time s is the inverse of the dual history's size at coalescent time R(s).

theorem sizeFn_eq_inv_dual (h : PiecewiseHistory K) (hK : 0 < K) {s : ℝ} (hs : 0 ≤ s) :
    h.sizeFn s = (h.dual.sizeFn (cumRate h.sizeFn s))⁻¹

Uses 7 · Used by 1

Statement usesPiecewise-constant population-size history · Dual history in coalescent time · Size function of a piecewise-constant history · Cumulative coalescence intensity

Proof usesCumulative rate is affine on each piece · Every nonnegative time lies in some piece · Size function on a piece equals the piece size

Used byBhaskar–Song identifiability

TheoremDual cumulative rate inverts the cumulative rate#✓fully proved

The dual cumulative rate inverts the cumulative rate.

theorem cumRate_dual_cumRate (h : PiecewiseHistory K) (hK : 0 < K) {s : ℝ} (hs : 0 ≤ s) :
    cumRate h.dual.sizeFn (cumRate h.sizeFn s) = s

Uses 7 · Used by 2

Statement usesPiecewise-constant population-size history · Dual history in coalescent time · Size function of a piecewise-constant history · Cumulative coalescence intensity

Proof usesCumulative rate is affine on each piece · Coalescent-time breakpoints are strictly increasing · Every nonnegative time lies in some piece

Used byTightness of n ≥ 2K · Bhaskar–Song identifiability

TheoremCumulative rate is strictly increasing#✓fully proved

The cumulative rate is strictly increasing on [0, ∞).

theorem cumRate_strictMonoOn (h : PiecewiseHistory K) (hK : 0 < K) :
    StrictMonoOn (cumRate h.sizeFn) (Set.Ici 0)

Uses 6 · Used by 1

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Cumulative coalescence intensity

Proof usesCumulative rate is affine on each piece · Every nonnegative time lies in some piece · Positivity of the piecewise size function

Used byBhaskar–Song identifiability

TheoremBhaskar–Song identifiability#✓fully proved

Bhaskar–Song identifiability (Bhaskar & Song 2014, Corollary 7, "determined" half, stated for the first-coalescence times): two piecewise-constant histories with K pieces whose expected first-coalescence times c_m agree for 2 ≤ m ≤ n, with n ≥ 2K, have the same population size at every time s ≥ 0. The proof writes C(m,2) c_m as an exponential sum in C(m,2) over at most 2K - 1 rates (choose_two_mul_firstCoalMean), identifies the coefficients with Real.eq_zero_of_sum_mul_exp_eq_zero, recovers the size as a function of coalescent time (the dual history) and inverts R (cumRate_dual_cumRate).

theorem sizeFn_eq_of_firstCoalMean_eq {n : ℕ} (h h' : PiecewiseHistory K) (hn : 2 * K ≤ n)
    (hc : ∀ m ∈ Icc 2 n, firstCoalMean h.sizeFn m = firstCoalMean h'.sizeFn m) :
    ∀ s, 0 ≤ s → h.sizeFn s = h'.sizeFn s

Uses 15

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Expected time to the first coalescence

Proof usesClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Cumulative rate is affine on each piece · Cumulative rate is strictly increasing · Dual history in coalescent time · Every nonnegative time lies in some piece · Size function on a piece equals the piece size · Size function is the inverse of the dual size in coalescent time · Monotonicity of piece start times · Nonnegativity of piece start times · Cumulative coalescence intensity · Exponential sums have full column rank

TheoremTightness of n ≥ 2K#✓fully proved

Tightness of n ≥ 2K (Bhaskar & Song 2014, Corollary 7): for every K ≥ 2 there are two piecewise-constant histories with K pieces whose sizes differ at some time s ≥ 0 but whose first-coalescence times c_m agree for 2 ≤ m ≤ 2K - 1; so sizeFn_eq_of_firstCoalMean_eq fails for n = 2K - 1. The construction is explicit: with z = 2^{-C(m,2)}, the two histories have coalescent-time breakpoints (2j - 1) log 2 and 2j log 2, so C(m,2) (c_m - c'_m) is a polynomial of degree 2K - 2 in z; its coefficients are those of ∏_{m=2}^{2K-1} (X - 2^{-C(m,2)}), which vanishes at the 2K - 2 points and has a nonzero constant term (the sizes at time 0 differ).

theorem exists_ne_firstCoalMean_eq_of_lt (K : ℕ) (hK : 2 ≤ K) :
    ∃ h h' : PiecewiseHistory K, (∃ s, 0 ≤ s ∧ h.sizeFn s ≠ h'.sizeFn s) ∧
      ∀ m ∈ Icc 2 (2 * K - 1), firstCoalMean h.sizeFn m = firstCoalMean h'.sizeFn m

Uses 10 · Used by 2

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Expected time to the first coalescence

Proof usesClosed form of the first-coalescence times · Dual cumulative rate inverts the cumulative rate · Coalescent-time breakpoints are strictly increasing · Dual history in coalescent time · Size function on a piece equals the piece size · Nonnegativity of piece start times · Cumulative coalescence intensity

Used byNon-identifiability from a bounded sample size · Distinct two-piece histories with equal first-coalescence times

TheoremMeasurability of the piecewise size function#✓fully proved

The size function is measurable.

theorem measurable_sizeFn (h : PiecewiseHistory K) : Measurable h.sizeFn

Uses 2 · Used by 1

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history

Used byNon-identifiability from a bounded sample size

TheoremSize function lies between the extreme piece sizes#✓fully proved

On [0, ∞) the size function lies between the smallest and the largest piece size.

theorem exists_le_sizeFn_le (h : PiecewiseHistory K) (hK : 0 < K) :
    ∃ a b : ℝ, 0 < a ∧ ∀ s, 0 ≤ s → a ≤ h.sizeFn s ∧ h.sizeFn s ≤ b

Uses 4 · Used by 1

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history

Proof usesEvery nonnegative time lies in some piece · Size function on a piece equals the piece size

Used byNon-identifiability from a bounded sample size

TheoremSize function is locally constant to the right#✓fully proved

The size function is constant on an interval to the right of every s ≥ 0.

theorem exists_sizeFn_eq_Ico (h : PiecewiseHistory K) (hK : 0 < K) {s : ℝ} (hs : 0 ≤ s) :
    ∃ ε > 0, ∀ r ∈ Set.Ico s (s + ε), h.sizeFn r = h.sizeFn s

Uses 4 · Used by 1

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history

Proof usesEvery nonnegative time lies in some piece · Size function on a piece equals the piece size

Used byNon-identifiability from a bounded sample size

TheoremDistinct two-piece histories with equal first-coalescence times#✓fully proved

The two-piece case of exists_ne_firstCoalMean_eq_of_lt.

@[deprecated "Use `exists_ne_firstCoalMean_eq_of_lt 2`." (since := "2026-11-02")]
theorem exists_ne_firstCoalMean_eq_two :
    ∃ h h' : PiecewiseHistory 2, (∃ s, 0 ≤ s ∧ h.sizeFn s ≠ h'.sizeFn s) ∧
      ∀ m ∈ Icc 2 3, firstCoalMean h.sizeFn m = firstCoalMean h'.sizeFn m

Uses 4

Statement usesPiecewise-constant population-size history · Size function of a piecewise-constant history · Expected time to the first coalescence

Proof usesTightness of n ≥ 2K

TheoremFirst-coalescence times depend only on sizes at nonnegative times#✓fully proved

Only the values on [0, ∞) enter the first-coalescence times.

theorem firstCoalMean_comp_max (η : ℝ → ℝ) (m : ℕ) :
    firstCoalMean (fun s => η (max s 0)) m = firstCoalMean η m

Uses 2 · Used by 1

Statement usesExpected time to the first coalescence

Proof usesCumulative coalescence intensity

Used byNon-identifiability from a bounded sample size

TheoremNon-identifiability from a bounded sample size#✓fully proved

For every n there are two measurable population-size functions, bounded between positive constants and different on a set of positive measure in [0, ∞), with the same c_m for 2 ≤ m ≤ n (two (n + 2)-piece histories from PiecewiseHistory.exists_ne_firstCoalMean_eq_of_lt, extended to s < 0 by their size at 0). This is the finite-sample shape of the statement of Myers, Fefferman & Patterson (2008); their theorem gives one pair of functions with equal c_m for every m.

theorem exists_ne_ae_firstCoalMean_eq_Icc (n : ℕ) :
    ∃ η₁ η₂ : ℝ → ℝ, Measurable η₁ ∧ Measurable η₂ ∧
      (∃ a b : ℝ, 0 < a ∧ ∀ s, a ≤ η₁ s ∧ η₁ s ≤ b ∧ a ≤ η₂ s ∧ η₂ s ≤ b) ∧
      ¬ (η₁ =ᵐ[volume.restrict (Set.Ici 0)] η₂) ∧
      ∀ m ∈ Icc 2 n, firstCoalMean η₁ m = firstCoalMean η₂ m

Uses 8

Statement usesExpected time to the first coalescence

Proof usesPiecewise-constant population-size history · Size function lies between the extreme piece sizes · Tightness of n ≥ 2K · Size function is locally constant to the right · Measurability of the piecewise size function · Size function of a piecewise-constant history · First-coalescence times depend only on sizes at nonnegative times

TheoremNon-identifiability of general histories#●ready to prove

Non-identifiability of general histories (Myers, Fefferman & Patterson 2008): there are two measurable population-size functions, bounded between positive constants, that differ on a set of positive Lebesgue measure in [0, ∞) and have the same expected first-coalescence time c_m for every m ≥ 2 (hence the same expected SFS for every sample size).

theorem_wanted exists_ne_ae_firstCoalMean_eq :
    ∃ η₁ η₂ : ℝ → ℝ, Measurable η₁ ∧ Measurable η₂ ∧
      (∃ a b : ℝ, 0 < a ∧ ∀ s, a ≤ η₁ s ∧ η₁ s ≤ b ∧ a ≤ η₂ s ∧ η₂ s ≤ b) ∧
      ¬ (η₁ =ᵐ[volume.restrict (Set.Ici 0)] η₂) ∧
      ∀ m, 2 ≤ m → firstCoalMean η₁ m = firstCoalMean η₂ m

Sources

• Myers, Fefferman & Patterson (2008).

Uses 1

Statement usesExpected time to the first coalescence

42 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.