Wright–Fisher semigroup and moment duality

TheoremCauchy property of uniform contractions extends from a dense set#✓fully proved

Uniformly contractive operators that are Cauchy on a dense set are Cauchy everywhere.

theorem cauchySeq_apply_of_dense {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {L : ℕ → E →L[ℝ] E} (hL : ∀ M, ‖L M‖ ≤ 1) {D : Set E}
    (hD : Dense D) (h : ∀ d ∈ D, CauchySeq fun M => L M d) (f : E) :
    CauchySeq fun M => L M f

Used by 1

Used byRescaled Wright–Fisher iterates form a Cauchy sequence

TheoremLimits of uniform contractions extend from a dense set#✓fully proved

Limits of uniformly contractive operators extend from a dense set to the whole space.

theorem tendsto_apply_of_dense {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {ι : Type*} {l : Filter ι} {T : ι → E →L[ℝ] E}
    (hT : ∀ i, ‖T i‖ ≤ 1) {S : E →L[ℝ] E} (hS : ‖S‖ ≤ 1) {D : Set E}
    (hD : Dense D) (h : ∀ d ∈ D, Tendsto (fun i => T i d) l (𝓝 (S d))) (f : E) :
    Tendsto (fun i => T i f) l (𝓝 (S f))

Used by 1

Used byStrong continuity

TheoremWeierstrass approximation theorem on the unit interval#✓fully proved

Weierstrass approximation: polynomial functions are dense in C([0, 1], ℝ).

theorem dense_polynomialFunctions : Dense (polynomialFunctions I : Set C(I, ℝ))

Used by 3

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Strong continuity · Semigroup law

TheoremNatural floor of a nonpositive multiple is zero#✓fully proved

If t ≤ 0, then the natural floor of t * M is zero.

theorem floor_mul_eq_zero {t : ℝ} (ht : t ≤ 0) (M : ℕ) : ⌊t * M⌋₊ = 0

Used by 2

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Wright–Fisher semigroup at nonpositive times is the identity

TheoremPowers of a unital endomorphism fix the constant function#✓fully proved

Every power of a continuous linear endomorphism fixing 1 also fixes 1.

theorem pow_apply_one {R E : Type*} [Semiring R] [TopologicalSpace E] [AddCommMonoid E]
    [Module R E] [One E] (T : E →L[R] E) (hT : T 1 = 1) (n : ℕ) :
    (T ^ n) 1 = 1

Used by 1

Used byWright–Fisher diffusion semigroup fixes constants

TheoremPowers of a positive endomorphism are positive#✓fully proved

Every power of a positive continuous linear endomorphism is positive.

theorem pow_nonneg {R E : Type*} [Semiring R] [TopologicalSpace E] [AddCommMonoid E]
    [Module R E] [PartialOrder E] (T : E →L[R] E)
    (hT : ∀ {f : E}, 0 ≤ f → 0 ≤ T f) (n : ℕ) {f : E} (hf : 0 ≤ f) :
    0 ≤ (T ^ n) f

Used by 1

Used byPositivity

DefinitionOne generation of the neutral Wright–Fisher chain#✓fully proved

One generation of the neutral Wright–Fisher chain with M gene copies, acting on continuous functions of the allele frequency: (wfStep M f)(x) = ∑_k f(k/M) C(M, k) x^k (1 - x)^(M - k), which for M ≥ 1 is the expected value of f at the next frequency Bin(M, x) / M (the M-th Bernstein operator, Mathlib's bernsteinApproximation; the expectation is ProbabilityTheory.integral_binomial). It is a linear contraction. At M = 0 it returns the constant f 0 (Lean's k / 0 = 0; no population).

MathlibExt.Biology.PopulationGenetics.Diffusion.WrightFisherSemigroup.wfStep · 18 lines

noncomputable def wfStep (M : ℕ) : C(I, ℝ) →L[ℝ] C(I, ℝ) :=
  LinearMap.mkContinuous
    { toFun := bernsteinApproximation M
      map_add' := fun f g => by
        ext x
        simp [bernsteinApproximation.apply, mul_add, Finset.sum_add_distrib]
      map_smul' := fun c f => by
        ext x
        simp [bernsteinApproximation.apply, Finset.mul_sum, smul_eq_mul, mul_left_comm] }
    1 (fun f => by
      refine (ContinuousMap.norm_le _ (by positivity)).2 fun x => ?_
      simp only [LinearMap.coe_mk, AddHom.coe_mk, one_mul, bernsteinApproximation.apply]
      calc ‖∑ k : Fin (M + 1), bernstein M k x • f (bernstein.z k)‖
          ≤ ∑ k : Fin (M + 1), ‖bernstein M k x • f (bernstein.z k)‖ := norm_sum_le _ _
        _ ≤ ∑ k : Fin (M + 1), bernstein M k x * ‖f‖ := Finset.sum_le_sum fun k _ => by
            rw [norm_smul, Real.norm_of_nonneg bernstein_nonneg]
            exact mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) bernstein_nonneg
        _ = ‖f‖ := by rw [← Finset.sum_mul, bernstein.probability, one_mul])

Used by 16

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Contraction · One Wright–Fisher generation is a sup-norm contraction · Iterated Wright–Fisher generations are sup-norm contractions · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · Convergence on polynomials · Neutral Wright–Fisher diffusion semigroup · Wright–Fisher diffusion semigroup fixes constants · Positivity · Wright–Fisher semigroup at nonpositive times is the identity · Diffusion semigroup agrees with the dual semigroup on polynomials · Wright–Fisher step is the Bernstein operator · One Wright–Fisher generation fixes constants · One Wright–Fisher generation preserves nonnegativity · Moment duality, m generations · One Wright–Fisher generation acting on monomials

TheoremWright–Fisher step is the Bernstein operator#✓fully proved

wfStep M is the Bernstein approximation operator.

theorem wfStep_apply (M : ℕ) (f : C(I, ℝ)) : wfStep M f = bernsteinApproximation M f

Uses 1

Statement usesOne generation of the neutral Wright–Fisher chain

TheoremOne Wright–Fisher generation is a sup-norm contraction#✓fully proved

One Wright–Fisher generation is a contraction for the sup norm.

theorem norm_wfStep_le (M : ℕ) : ‖wfStep M‖ ≤ 1

Uses 1 · Used by 1

Statement usesOne generation of the neutral Wright–Fisher chain

Used byIterated Wright–Fisher generations are sup-norm contractions

TheoremOne Wright–Fisher generation fixes constants#✓fully proved

One Wright–Fisher generation fixes the constant function 1.

theorem wfStep_apply_one (M : ℕ) : wfStep M 1 = 1

Uses 1 · Used by 1

Statement usesOne generation of the neutral Wright–Fisher chain

Used byWright–Fisher diffusion semigroup fixes constants

TheoremOne Wright–Fisher generation preserves nonnegativity#✓fully proved

One Wright–Fisher generation maps nonnegative functions to nonnegative functions.

theorem wfStep_nonneg (M : ℕ) {f : C(I, ℝ)} (hf : 0 ≤ f) : 0 ≤ wfStep M f

Uses 1 · Used by 1

Statement usesOne generation of the neutral Wright–Fisher chain

Used byPositivity

TheoremIterated Wright–Fisher generations are sup-norm contractions#✓fully proved

Any number of Wright–Fisher generations is a contraction for the sup norm.

theorem norm_wfStep_pow_le (M m : ℕ) : ‖wfStep M ^ m‖ ≤ 1

Uses 2 · Used by 3

Statement usesOne generation of the neutral Wright–Fisher chain

Proof usesOne Wright–Fisher generation is a sup-norm contraction

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Contraction · Neutral Wright–Fisher diffusion semigroup

TheoremMoment duality, one generation (polynomial identity)#✓fully proved

For M ≥ 1 gene copies, ∑_i C(M, i) x^i (1 - x)^(M - i) (i/M)^n = ∑_k S(n, k) M_(k) / M^n · x^k: the n-th moment of the frequency after one generation equals the generating function of the number of distinct parents of n sampled genes. Holds for every real x.

theorem sum_binomial_mul_div_pow (M n : ℕ) (hM : M ≠ 0) (x : ℝ) :
    ∑ i ∈ Finset.range (M + 1),
        (M.choose i : ℝ) * x ^ i * (1 - x) ^ (M - i) * ((i : ℝ) / M) ^ n =
      ∑ k ∈ Finset.range (n + 1), wfLineageProb M n k * x ^ k

Sources

• Ethier & Griffiths (1993); Durrett (2008), §7.

Uses 1 · Used by 2

Statement usesWright–Fisher transition probability of the lineage count

Used byMoment duality, one generation · One Wright–Fisher generation acting on monomials

TheoremMoment duality, one generation#✓fully proved

If the allele count after one neutral Wright–Fisher generation with M ≥ 1 gene copies is Bin(M, x), then E_x[(X₁)^n] = ∑_k wfLineageProb M n k · x^k, where X₁ is the new frequency and wfLineageProb M n k is the probability that n genes have k distinct parents.

theorem integral_binomial_div_pow (M n : ℕ) (hM : M ≠ 0) (x : I) :
    ∫ i, ((i : ℝ) / M) ^ n ∂(ProbabilityTheory.binomial M x) =
      ∑ k ∈ Finset.range (n + 1), wfLineageProb M n k * (x : ℝ) ^ k

Uses 2

Statement usesWright–Fisher transition probability of the lineage count

Proof usesMoment duality, one generation (polynomial identity)

TheoremOne Wright–Fisher generation acting on monomials#✓fully proved

One generation maps x ^ n to ∑_k wfLineageProb M n k x ^ k.

theorem wfStep_X_pow (M n : ℕ) (hM : M ≠ 0) :
    wfStep M ((X ^ n : ℝ[X]).toContinuousMapOn I) =
      (∑ k ∈ Finset.range (n + 1), C (wfLineageProb M n k) * X ^ k).toContinuousMapOn I

Uses 3 · Used by 1

Statement usesWright–Fisher transition probability of the lineage count · One generation of the neutral Wright–Fisher chain

Proof usesMoment duality, one generation (polynomial identity)

Used byMoment duality, m generations

TheoremMoment duality, m generations#✓fully proved

For M ≥ 1 and n ≤ N, m generations of the Wright–Fisher chain map x ^ n to ∑_k ((wfLineageMatrix N M)^m) n k · x^k: the n-th moment of the frequency after m generations is the generating function of the number of ancestors, m generations back, of n sampled genes.

theorem wfStep_pow_X_pow (M m N : ℕ) (hM : M ≠ 0) (n : Fin (N + 1)) :
    (wfStep M ^ m) ((X ^ (n : ℕ) : ℝ[X]).toContinuousMapOn I) =
      (∑ k : Fin (N + 1),
        C ((wfLineageMatrix N M ^ m) n k) * X ^ (k : ℕ)).toContinuousMapOn I

Uses 4 · Used by 1

Statement usesWright–Fisher transition matrix of the lineage count · One generation of the neutral Wright–Fisher chain

Proof usesWright–Fisher transition probability of the lineage count · One Wright–Fisher generation acting on monomials

Used byConvergence on polynomials

DefinitionDual moment polynomial of Kingman's coalescent#✓fully proved

The dual moment polynomial ∑_k P_t(n → k) X^k, where for t ≥ 0, P_t(n → k) = exp (t • G) n k is the probability that n lineages of Kingman's coalescent have k ancestors time t earlier (time in units of M = 2N generations); evaluated at x it is E_n[x^{A_t}] for the block-counting process A.

noncomputable def dualMomentPoly (t : ℝ) (n : ℕ) : ℝ[X] :=
  ∑ k : Fin (n + 1),
    C (NormedSpace.exp (t • blockCountingGenerator n) (Fin.last n) k) * X ^ (k : ℕ)

Uses 1 · Used by 9

Statement usesGenerator of Kingman's block-counting process

Used byWright–Fisher semigroup on polynomials by moment duality · Semigroup law · Dual semigroup fixes the constant polynomial one · Dual semigroup on a monomial · Dual semigroup at time zero is the identity · Strong continuity · Generator on polynomials · Convergence on polynomials · Moment duality for the diffusion

DefinitionWright–Fisher semigroup on polynomials by moment duality#✓fully proved

The neutral Wright–Fisher diffusion semigroup on polynomials, defined by moment duality on the monomial basis: polySemigroup t (X ^ n) = dualMomentPoly t n. It is meaningful for t ≥ 0; the formula is defined, and the group law holds, for every real t.

noncomputable def polySemigroup (t : ℝ) : ℝ[X] →ₗ[ℝ] ℝ[X] :=
  (Polynomial.basisMonomials ℝ).constr ℝ (dualMomentPoly t)

Uses 1 · Used by 11

Statement usesDual moment polynomial of Kingman's coalescent

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Semigroup law · Dual semigroup fixes the constant polynomial one · Dual semigroup on a monomial · Dual semigroup at time zero is the identity · Strong continuity · Generator on polynomials · Convergence on polynomials · Semigroup law · Diffusion semigroup agrees with the dual semigroup on polynomials · Moment duality for the diffusion

TheoremDual semigroup on a monomial#✓fully proved

The dual semigroup on a monomial is the dual moment polynomial.

theorem polySemigroup_X_pow (t : ℝ) (n : ℕ) : polySemigroup t (X ^ n) = dualMomentPoly t n

Uses 2 · Used by 7

Statement usesDual moment polynomial of Kingman's coalescent · Wright–Fisher semigroup on polynomials by moment duality

Used bySemigroup law · Dual semigroup fixes the constant polynomial one · Dual semigroup at time zero is the identity · Strong continuity · Generator on polynomials · Convergence on polynomials · Moment duality for the diffusion

TheoremDual semigroup at time zero is the identity#✓fully proved

At time 0 the dual semigroup is the identity.

theorem polySemigroup_zero : polySemigroup 0 = LinearMap.id

Uses 4 · Used by 2

Statement usesWright–Fisher semigroup on polynomials by moment duality

Proof usesGenerator of Kingman's block-counting process · Dual moment polynomial of Kingman's coalescent · Dual semigroup on a monomial

Used byStrong continuity · Generator on polynomials

TheoremSemigroup law#✓fully proved

Semigroup law on polynomials, from exp ((s + t) • G) = exp (t • G) * exp (s • G) and truncation consistency; holds for all real s, t.

theorem polySemigroup_add (s t : ℝ) :
    polySemigroup (s + t) = polySemigroup s ∘ₗ polySemigroup t

Uses 6 · Used by 1

Statement usesWright–Fisher semigroup on polynomials by moment duality

Proof usesGenerator of Kingman's block-counting process · Truncation consistency · The block-counting process never gains lineages · Dual moment polynomial of Kingman's coalescent · Dual semigroup on a monomial

Used bySemigroup law

TheoremDual semigroup fixes the constant polynomial one#✓fully proved

The dual semigroup fixes the constant polynomial 1 (zero lineages stay zero).

theorem polySemigroup_one (t : ℝ) : polySemigroup t 1 = 1

Uses 4

Statement usesWright–Fisher semigroup on polynomials by moment duality

Proof usesGenerator of Kingman's block-counting process · Dual moment polynomial of Kingman's coalescent · Dual semigroup on a monomial

TheoremConvergence on polynomials#✓fully proved

For t ≥ 0 and every polynomial p, ⌊tM⌋ generations of the Wright–Fisher chain with M gene copies applied to p converge uniformly on [0, 1] to polySemigroup t p as M → ∞ (moment duality plus Kingman's theorem for the lineage count).

theorem tendsto_wfStep_pow_floor_toContinuousMapOn (p : ℝ[X]) {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun M : ℕ => (wfStep M ^ ⌊t * M⌋₊) (p.toContinuousMapOn I)) atTop
      (𝓝 ((polySemigroup t p).toContinuousMapOn I))

Uses 8 · Used by 2

Statement usesWright–Fisher semigroup on polynomials by moment duality · One generation of the neutral Wright–Fisher chain

Proof usesGenerator of Kingman's block-counting process · Kingman's theorem for the lineage count · Wright–Fisher transition matrix of the lineage count · Dual moment polynomial of Kingman's coalescent · Dual semigroup on a monomial · Moment duality, m generations

Used byRescaled Wright–Fisher iterates form a Cauchy sequence · Diffusion semigroup agrees with the dual semigroup on polynomials

TheoremRescaled Wright–Fisher iterates form a Cauchy sequence#✓fully proved

For every continuous f, the sequence (wfStep M)^⌊tM⌋ f is Cauchy in C([0, 1], ℝ): it converges on the dense set of polynomials and the operators are contractions.

theorem cauchySeq_wfStep_pow_floor (t : ℝ) (f : C(I, ℝ)) :
    CauchySeq fun M : ℕ => (wfStep M ^ ⌊t * M⌋₊) f

Uses 7 · Used by 3

Statement usesOne generation of the neutral Wright–Fisher chain

Proof usesCauchy property of uniform contractions extends from a dense set · Weierstrass approximation theorem on the unit interval · Natural floor of a nonpositive multiple is zero · Iterated Wright–Fisher generations are sup-norm contractions · Wright–Fisher semigroup on polynomials by moment duality · Convergence on polynomials

Used byContraction · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · Neutral Wright–Fisher diffusion semigroup

DefinitionNeutral Wright–Fisher diffusion semigroup#✓fully proved

The neutral Wright–Fisher diffusion semigroup on C([0, 1], ℝ), time in units of M = 2N generations: wfSemigroup t f is the uniform limit of (wfStep M)^⌊tM⌋ f as M → ∞ (tendsto_wfStep_pow_floor). For t < 0 it is the identity (a junk value: ⌊tM⌋₊ = 0).

MathlibExt.Biology.PopulationGenetics.Diffusion.WrightFisherSemigroup.wfSemigroup · 16 lines

noncomputable def wfSemigroup (t : ℝ) : C(I, ℝ) →L[ℝ] C(I, ℝ) :=
  LinearMap.mkContinuous
    { toFun := fun f => limUnder atTop fun M : ℕ => (wfStep M ^ ⌊t * M⌋₊) f
      map_add' := fun f g => by
        refine tendsto_nhds_unique (cauchySeq_wfStep_pow_floor t (f + g)).tendsto_limUnder ?_
        simpa using ((cauchySeq_wfStep_pow_floor t f).tendsto_limUnder).add
          (cauchySeq_wfStep_pow_floor t g).tendsto_limUnder
      map_smul' := fun c f => by
        refine tendsto_nhds_unique (cauchySeq_wfStep_pow_floor t (c • f)).tendsto_limUnder ?_
        simpa using ((cauchySeq_wfStep_pow_floor t f).tendsto_limUnder).const_smul c }
    1 (fun f => by
      simp only [LinearMap.coe_mk, AddHom.coe_mk, one_mul]
      refine le_of_tendsto ((cauchySeq_wfStep_pow_floor t f).tendsto_limUnder).norm
        (Eventually.of_forall fun M => ?_)
      exact ((wfStep M ^ ⌊t * M⌋₊).le_opNorm f).trans
        (mul_le_of_le_one_left (norm_nonneg f) (norm_wfStep_pow_le M _)))

Uses 3 · Used by 21

Statement usesRescaled Wright–Fisher iterates form a Cauchy sequence · Iterated Wright–Fisher generations are sup-norm contractions · One generation of the neutral Wright–Fisher chain

Used byKolmogorov continuity condition for the raw Wright–Fisher process · Polynomial semigroup dynamics · Wright–Fisher transition kernel represents the semigroup · Kernel form of Wright–Fisher moment duality · Contraction · Strong continuity · Generator on polynomials · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · Semigroup law · Wright–Fisher diffusion semigroup fixes constants · Fourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Positivity · Wright–Fisher semigroup at nonpositive times is the identity · Wright–Fisher semigroup as a positive operator · Semigroup law for the positive Wright–Fisher operator · Action of the positive Wright–Fisher operator · Second-moment bound for the Wright–Fisher semigroup · Diffusion semigroup agrees with the dual semigroup on polynomials · Moment duality for the diffusion · Wright–Fisher diffusion semigroup at time zero is the identity · Wright–Fisher transition kernel is the identity at nonpositive times

TheoremDiffusion approximation of the transition operators (Trotter–Kato, concrete form)#✓fully proved

For every continuous f, ⌊tM⌋ generations of the neutral Wright–Fisher chain with M gene copies applied to f converge uniformly on [0, 1] to wfSemigroup t f.

theorem tendsto_wfStep_pow_floor (t : ℝ) (f : C(I, ℝ)) :
    Tendsto (fun M : ℕ => (wfStep M ^ ⌊t * M⌋₊) f) atTop (𝓝 (wfSemigroup t f))

Sources

• Ethier & Kurtz (1986), ch. 1, §6 (approximation theorems), and ch. 10.

Uses 3 · Used by 4

Statement usesNeutral Wright–Fisher diffusion semigroup · One generation of the neutral Wright–Fisher chain

Proof usesRescaled Wright–Fisher iterates form a Cauchy sequence

Used byWright–Fisher diffusion semigroup fixes constants · Positivity · Wright–Fisher semigroup at nonpositive times is the identity · Diffusion semigroup agrees with the dual semigroup on polynomials

TheoremContraction#✓fully proved

sup_{[0,1]} |wfSemigroup t f| ≤ sup_{[0,1]} |f|.

theorem norm_wfSemigroup_le (t : ℝ) : ‖wfSemigroup t‖ ≤ 1

Uses 4 · Used by 2

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesRescaled Wright–Fisher iterates form a Cauchy sequence · Iterated Wright–Fisher generations are sup-norm contractions · One generation of the neutral Wright–Fisher chain

Used byPolynomial semigroup dynamics · Strong continuity

TheoremDiffusion semigroup agrees with the dual semigroup on polynomials#✓fully proved

On polynomials the diffusion semigroup is the dual semigroup, for t ≥ 0.

theorem wfSemigroup_toContinuousMapOn {t : ℝ} (ht : 0 ≤ t) (p : ℝ[X]) :
    wfSemigroup t (p.toContinuousMapOn I) = (polySemigroup t p).toContinuousMapOn I

Uses 5 · Used by 4

Statement usesWright–Fisher semigroup on polynomials by moment duality · Neutral Wright–Fisher diffusion semigroup

Proof usesDiffusion approximation of the transition operators (Trotter–Kato, concrete form) · Convergence on polynomials · One generation of the neutral Wright–Fisher chain

Used byStrong continuity · Generator on polynomials · Semigroup law · Moment duality for the diffusion

TheoremWright–Fisher semigroup at nonpositive times is the identity#✓fully proved

For t ≤ 0, wfSemigroup t is the identity (at t = 0 by definition of a semigroup; for t < 0 this is a junk value of the definition).

theorem wfSemigroup_of_nonpos {t : ℝ} (ht : t ≤ 0) : wfSemigroup t = 1

Uses 4 · Used by 2

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesNatural floor of a nonpositive multiple is zero · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · One generation of the neutral Wright–Fisher chain

Used byWright–Fisher diffusion semigroup at time zero is the identity · Wright–Fisher transition kernel is the identity at nonpositive times

TheoremWright–Fisher diffusion semigroup at time zero is the identity#✓fully proved

At time 0 the diffusion semigroup is the identity.

@[simp]
theorem wfSemigroup_zero : wfSemigroup 0 = 1

Uses 2 · Used by 2

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesWright–Fisher semigroup at nonpositive times is the identity

Used byFourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Second-moment bound for the Wright–Fisher semigroup

TheoremMoment duality for the diffusion#✓fully proved

Moment duality for the diffusion (Ethier & Griffiths 1993). For t ≥ 0, the semigroup applied to x ↦ x ^ n is ∑_k P_t(n → k) x^k, with P_t = exp (t • G) the transition matrix of Kingman's block-counting process A; in process language E_x[(X_t)^n] = E_n[x^{A_t}] (the processes themselves are not constructed here).

theorem wfSemigroup_X_pow {t : ℝ} (ht : 0 ≤ t) (n : ℕ) (x : I) :
    wfSemigroup t ((X ^ n : ℝ[X]).toContinuousMapOn I) x =
      ∑ k : Fin (n + 1),
        NormedSpace.exp (t • blockCountingGenerator n) (Fin.last n) k * (x : ℝ) ^ (k : ℕ)

Uses 6 · Used by 1

Statement usesGenerator of Kingman's block-counting process · Neutral Wright–Fisher diffusion semigroup

Proof usesDual moment polynomial of Kingman's coalescent · Wright–Fisher semigroup on polynomials by moment duality · Dual semigroup on a monomial · Diffusion semigroup agrees with the dual semigroup on polynomials

Used byKernel form of Wright–Fisher moment duality

TheoremSemigroup law#✓fully proved

Semigroup law for s, t ≥ 0.

theorem wfSemigroup_add {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) :
    wfSemigroup (s + t) = wfSemigroup s * wfSemigroup t

Uses 5 · Used by 2

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesWeierstrass approximation theorem on the unit interval · Wright–Fisher semigroup on polynomials by moment duality · Semigroup law · Diffusion semigroup agrees with the dual semigroup on polynomials

Used byPolynomial semigroup dynamics · Semigroup law for the positive Wright–Fisher operator

TheoremWright–Fisher diffusion semigroup fixes constants#✓fully proved

The diffusion semigroup fixes constants (it is Markov: total mass 1).

theorem wfSemigroup_apply_one (t : ℝ) : wfSemigroup t 1 = 1

Uses 5 · Used by 2

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesPowers of a unital endomorphism fix the constant function · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · One generation of the neutral Wright–Fisher chain · One Wright–Fisher generation fixes constants

Used byPositive Wright–Fisher operator fixes constants · Second-moment bound for the Wright–Fisher semigroup

TheoremPositivity#✓fully proved

The diffusion semigroup maps nonnegative functions to nonnegative functions.

theorem wfSemigroup_nonneg (t : ℝ) {f : C(I, ℝ)} (hf : 0 ≤ f) : 0 ≤ wfSemigroup t f

Uses 5 · Used by 3

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesPowers of a positive endomorphism are positive · Diffusion approximation of the transition operators (Trotter–Kato, concrete form) · One generation of the neutral Wright–Fisher chain · One Wright–Fisher generation preserves nonnegativity

Used byFourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Wright–Fisher semigroup as a positive operator · Second-moment bound for the Wright–Fisher semigroup

TheoremStrong continuity#✓fully proved

wfSemigroup t f → f uniformly as t → 0⁺, for every continuous f.

theorem tendsto_wfSemigroup_nhdsGE_zero (f : C(I, ℝ)) :
    Tendsto (fun t => wfSemigroup t f) (𝓝[≥] 0) (𝓝 f)

Uses 14 · Used by 3

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Left eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator · Spectral decomposition of the block-counting transition matrix · Weierstrass approximation theorem on the unit interval · Limits of uniform contractions extend from a dense set · Dual moment polynomial of Kingman's coalescent · Contraction · Wright–Fisher semigroup on polynomials by moment duality · Dual semigroup on a monomial · Dual semigroup at time zero is the identity · Diffusion semigroup agrees with the dual semigroup on polynomials

Used byPolynomial semigroup dynamics · Fourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Second-moment bound for the Wright–Fisher semigroup

DefinitionNeutral Wright–Fisher generator on polynomials#✓fully proved

The neutral Wright–Fisher generator on polynomials, x (1 - x) / 2 · p''.

noncomputable def polyGenerator (p : ℝ[X]) : ℝ[X] :=
  C (1 / 2 : ℝ) * X * (1 - X) * derivative (derivative p)

Used by 5

Used byPolynomial generator agrees with the neutral Wright–Fisher generator · Polynomial semigroup dynamics · Generator on polynomials · Fourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Second-moment bound for the Wright–Fisher semigroup

TheoremPolynomial generator agrees with the neutral Wright–Fisher generator#✓fully proved

polyGenerator is the neutral Wright–Fisher generator generator 0 evaluated on p.

theorem eval_polyGenerator (p : ℝ[X]) (x : ℝ) :
    (polyGenerator p).eval x = generator 0 (fun y => p.eval y) x

Uses 2 · Used by 1

Statement usesNeutral Wright–Fisher generator on polynomials · Backward generator of the Wright–Fisher diffusion with selection

Used byGenerator on polynomials

TheoremGenerator on polynomials#✓fully proved

For every polynomial p, (wfSemigroup t p - p) / t → x (1 - x) / 2 · p'' uniformly on [0, 1] as t → 0⁺.

theorem tendsto_wfSemigroup_sub_div (p : ℝ[X]) :
    Tendsto (fun t : ℝ => t⁻¹ • (wfSemigroup t (p.toContinuousMapOn I) - p.toContinuousMapOn I))
      (𝓝[>] 0) (𝓝 ((polyGenerator p).toContinuousMapOn I))

Sources

• Ethier & Kurtz (1986), ch. 10; Durrett (2008), §7.

Uses 17 · Used by 1

Statement usesNeutral Wright–Fisher generator on polynomials · Neutral Wright–Fisher diffusion semigroup

Proof usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Right eigenvector equation for the block-counting generator · Left eigenvectors of Kingman's block-counting generator · Left and right eigenvector matrices are mutually inverse · Right eigenvectors of Kingman's block-counting generator · Spectral decomposition of the block-counting transition matrix · Dual moment polynomial of Kingman's coalescent · Polynomial generator agrees with the neutral Wright–Fisher generator · Wright–Fisher semigroup on polynomials by moment duality · Dual semigroup on a monomial · Dual semigroup at time zero is the identity · Diffusion semigroup agrees with the dual semigroup on polynomials · Backward generator of the Wright–Fisher diffusion with selection · Moment duality with Kingman's coalescent

Used byPolynomial semigroup dynamics

TheoremPolynomial semigroup dynamics#✓fully proved

At every positive time, differentiating the existing Wright–Fisher semigroup on a polynomial equals applying the semigroup to its generator.

theorem hasDerivAt_wfSemigroup_toContinuousMapOn (p : ℝ[X]) {t : ℝ} (ht : 0 < t) :
    HasDerivAt (fun s : ℝ => wfSemigroup s (p.toContinuousMapOn I))
      (wfSemigroup t ((polyGenerator p).toContinuousMapOn I)) t

Uses 6 · Used by 2

Statement usesNeutral Wright–Fisher generator on polynomials · Neutral Wright–Fisher diffusion semigroup

Proof usesContraction · Strong continuity · Generator on polynomials · Semigroup law

Used byFourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Second-moment bound for the Wright–Fisher semigroup

TheoremSecond-moment bound for the Wright–Fisher semigroup#✓fully proved

The centered second moment grows at most linearly: T_t[(y-x)²](x) ≤ t/4.

theorem wfSemigroup_second_increment_le {t : ℝ} (ht : 0 ≤ t) (x : I) :
    wfSemigroup t (((X - C (x : ℝ)) ^ 2 : ℝ[X]).toContinuousMapOn I) x ≤
      (1 / 4 : ℝ) * t

Uses 7 · Used by 1

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesPolynomial semigroup dynamics · Neutral Wright–Fisher generator on polynomials · Strong continuity · Wright–Fisher diffusion semigroup fixes constants · Positivity · Wright–Fisher diffusion semigroup at time zero is the identity

Used byFourth-moment Kolmogorov bound for the Wright–Fisher semigroup

TheoremFourth-moment Kolmogorov bound for the Wright–Fisher semigroup#✓fully proved

The fourth centered increment of the neutral Wright–Fisher semigroup satisfies the uniform Kolmogorov bound T_t[(y-x)⁴](x) ≤ (3/16)t².

theorem wfSemigroup_fourth_increment_le {t : ℝ} (ht : 0 ≤ t) (x : I) :
    wfSemigroup t (((X - C (x : ℝ)) ^ 4 : ℝ[X]).toContinuousMapOn I) x ≤
      (3 / 16 : ℝ) * t ^ 2

Uses 7 · Used by 1

Statement usesNeutral Wright–Fisher diffusion semigroup

Proof usesPolynomial semigroup dynamics · Neutral Wright–Fisher generator on polynomials · Strong continuity · Positivity · Second-moment bound for the Wright–Fisher semigroup · Wright–Fisher diffusion semigroup at time zero is the identity

Used byKolmogorov continuity condition for the raw Wright–Fisher process

DefinitionWright–Fisher semigroup as a positive operator#✓fully proved

The Wright–Fisher semigroup bundled as a positive continuous linear operator.

noncomputable def wfSemigroupPositive (t : ℝ) : C(I, ℝ) →P[ℝ] C(I, ℝ) :=
  PositiveContinuousLinearMap.mk
    (PositiveLinearMap.mk (wfSemigroup t).toLinearMap fun f g hfg => by
      have hgf : 0 ≤ g - f := ContinuousMap.le_def.mpr fun x =>
        sub_nonneg.mpr (ContinuousMap.le_def.mp hfg x)
      apply ContinuousMap.le_def.mpr
      intro x
      have hx := ContinuousMap.le_def.mp (wfSemigroup_nonneg t hgf) x
      rw [map_sub] at hx
      exact sub_nonneg.mp hx)
    (wfSemigroup t).continuous

Uses 2 · Used by 12

Statement usesNeutral Wright–Fisher diffusion semigroup · Positivity

Used byContinuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process · One-time marginals of the raw Wright–Fisher path measure · Two-time law of the raw Wright–Fisher path measure · Canonical path measure of the raw Wright–Fisher process · Wright–Fisher transition kernel represents the semigroup · Semigroup law for the positive Wright–Fisher operator · Action of the positive Wright–Fisher operator · Positive Wright–Fisher operator fixes constants · Transition kernel of the neutral Wright–Fisher diffusion · Chapman–Kolmogorov equation for the Wright–Fisher diffusion · Wright–Fisher transition kernel is the identity at nonpositive times

TheoremAction of the positive Wright–Fisher operator#✓fully proved

Bundling the operator as positive leaves its action on continuous functions unchanged.

@[simp]
theorem wfSemigroupPositive_apply (t : ℝ) (f : C(I, ℝ)) :
    wfSemigroupPositive t f = wfSemigroup t f

Uses 2 · Used by 1

Statement usesNeutral Wright–Fisher diffusion semigroup · Wright–Fisher semigroup as a positive operator

Used byWright–Fisher transition kernel represents the semigroup

TheoremPositive Wright–Fisher operator fixes constants#✓fully proved

The positive Wright–Fisher operator fixes the constant function 1.

@[simp]
theorem wfSemigroupPositive_apply_one (t : ℝ) : wfSemigroupPositive t 1 = 1

Uses 2 · Used by 9

Statement usesWright–Fisher semigroup as a positive operator

Proof usesWright–Fisher diffusion semigroup fixes constants

Used byContinuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process · One-time marginals of the raw Wright–Fisher path measure · Two-time law of the raw Wright–Fisher path measure · Canonical path measure of the raw Wright–Fisher process · Wright–Fisher transition kernel represents the semigroup · Transition kernel of the neutral Wright–Fisher diffusion · Chapman–Kolmogorov equation for the Wright–Fisher diffusion · Wright–Fisher transition kernel is the identity at nonpositive times

TheoremSemigroup law for the positive Wright–Fisher operator#✓fully proved

The positive-operator form of the Wright–Fisher semigroup law.

theorem wfSemigroupPositive_add {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) :
    wfSemigroupPositive (s + t) =
      (wfSemigroupPositive s).comp (wfSemigroupPositive t)

Uses 3 · Used by 1

Statement usesWright–Fisher semigroup as a positive operator

Proof usesNeutral Wright–Fisher diffusion semigroup · Semigroup law

Used byChapman–Kolmogorov equation for the Wright–Fisher diffusion

DefinitionTransition kernel of the neutral Wright–Fisher diffusion#✓fully proved

The transition kernel of the neutral Wright–Fisher diffusion at time t. For nonnegative t it is the probabilistic transition corresponding to wfSemigroup t; for negative t, both the operator and kernel are the identity junk value inherited from wfSemigroup.

noncomputable def wfTransitionKernel (t : ℝ) : Kernel I I :=
  markovKernelOfPositiveOperator (wfSemigroupPositive t) (wfSemigroupPositive_apply_one t)

Uses 3 · Used by 12

Statement usesWright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Markov kernel of a positive unital operator

Used byContinuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process · One-time marginals of the raw Wright–Fisher path measure · Two-time law of the raw Wright–Fisher path measure · Neutral Wright–Fisher transition kernel at nonnegative time · Canonical path measure of the raw Wright–Fisher process · Wright–Fisher transition kernel represents the semigroup · Kernel form of Wright–Fisher moment duality · Chapman–Kolmogorov equation for the Wright–Fisher diffusion · Wright–Fisher transition kernel is the identity at nonpositive times · Wright–Fisher transition kernel is the identity at time zero · Wright–Fisher transitions at time zero are Dirac masses

TheoremWright–Fisher transition kernel represents the semigroup#✓fully proved

Integration against the transition kernel agrees with the Wright–Fisher semigroup on every continuous test function and every initial allele frequency.

@[simp]
theorem integral_wfTransitionKernel (t : ℝ) (f : C(I, ℝ)) (x : I) :
    ∫ y, f y ∂wfTransitionKernel t x = wfSemigroup t f x

Uses 7 · Used by 3

Statement usesNeutral Wright–Fisher diffusion semigroup · Transition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher semigroup as a positive operator · Action of the positive Wright–Fisher operator · Positive Wright–Fisher operator fixes constants · Kernel of a positive operator represents it on continuous functions · Markov kernel of a positive unital operator

Used byKolmogorov continuity condition for the raw Wright–Fisher process · Kernel form of Wright–Fisher moment duality · Wright–Fisher transition kernel is the identity at nonpositive times

TheoremWright–Fisher transition kernel is the identity at nonpositive times#✓fully proved

For nonpositive times, the Wright–Fisher transition is the identity kernel.

theorem wfTransitionKernel_of_nonpos {t : ℝ} (ht : t ≤ 0) :
    wfTransitionKernel t = (Kernel.id : Kernel I I)

Uses 9 · Used by 1

Statement usesTransition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher transition kernel represents the semigroup · Neutral Wright–Fisher diffusion semigroup · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Wright–Fisher semigroup at nonpositive times is the identity · Positive-operator-to-Markov-kernel bridge · Markov kernels are determined by integrals of continuous functions · Markov kernel of a positive unital operator

Used byWright–Fisher transition kernel is the identity at time zero

TheoremWright–Fisher transition kernel is the identity at time zero#✓fully proved

At time zero the Wright–Fisher transition is the identity kernel.

@[simp]
theorem wfTransitionKernel_zero : wfTransitionKernel 0 = (Kernel.id : Kernel I I)

Uses 2 · Used by 2

Statement usesTransition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher transition kernel is the identity at nonpositive times

Used byTime-zero marginal of the raw path measure is the initial state · Wright–Fisher transitions at time zero are Dirac masses

TheoremWright–Fisher transitions at time zero are Dirac masses#✓fully proved

Pointwise identity law for the transition kernel at time zero.

@[simp]
theorem wfTransitionKernel_zero_apply (x : I) : wfTransitionKernel 0 x = Measure.dirac x

Uses 2

Statement usesTransition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher transition kernel is the identity at time zero

TheoremChapman–Kolmogorov equation for the Wright–Fisher diffusion#✓fully proved

Chapman–Kolmogorov law for the Wright–Fisher transition kernels. With Mathlib's convention, K_t ∘ₖ K_s first evolves for time s and then for time t.

theorem wfTransitionKernel_add {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) :
    wfTransitionKernel (s + t) = wfTransitionKernel t ∘ₖ wfTransitionKernel s

Uses 6 · Used by 1

Statement usesTransition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher semigroup as a positive operator · Semigroup law for the positive Wright–Fisher operator · Positive Wright–Fisher operator fixes constants · Markov kernel of a positive unital operator · Operator composition corresponds to kernel composition

Used byChapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel

TheoremKernel form of Wright–Fisher moment duality#✓fully proved

Kernel form of Wright–Fisher moment duality: transition-kernel moments are the transition probabilities of Kingman's block-counting process.

theorem integral_wfTransitionKernel_X_pow {t : ℝ} (ht : 0 ≤ t) (n : ℕ) (x : I) :
    ∫ y, ((Polynomial.X ^ n : Polynomial ℝ).toContinuousMapOn I) y ∂wfTransitionKernel t x =
      ∑ k : Fin (n + 1),
        NormedSpace.exp (t • blockCountingGenerator n) (Fin.last n) k * (x : ℝ) ^ (k : ℕ)

Uses 5

Statement usesGenerator of Kingman's block-counting process · Transition kernel of the neutral Wright–Fisher diffusion

Proof usesWright–Fisher transition kernel represents the semigroup · Neutral Wright–Fisher diffusion semigroup · Moment duality for the diffusion

52 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.