Construction of the neutral Wright–Fisher diffusion

AbbreviationCanonical sample paths of the raw Wright–Fisher process#✓fully proved

Canonical sample paths before continuous modification.

abbrev SamplePath := NNReal → I

Used by 12

Used byContinuous realization of the raw Wright–Fisher process · Continuous 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 · Time-zero marginal of the raw path measure is the initial state · Two-time law of the raw Wright–Fisher path measure · Modified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws · Continuous modified Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process · Normalized raw process agrees with the coordinates almost surely

DefinitionNeutral Wright–Fisher transition kernel at nonnegative time#✓fully proved

The neutral Wright--Fisher transition kernel at nonnegative time.

noncomputable def neutralKernel (t : NNReal) : Kernel I I :=
  wfTransitionKernel (t : ℝ)

Uses 1 · Used by 7

Statement usesTransition kernel of the neutral Wright–Fisher diffusion

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 · Time-zero marginal of the raw path measure is the initial state · Two-time law of the raw Wright–Fisher path measure · Chapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Canonical path measure of the raw Wright–Fisher process

TheoremChapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel#✓fully proved

Chapman--Kolmogorov for the nonnegative-time specialization.

theorem neutralKernel_add (s t : NNReal) :
    neutralKernel (s + t) = neutralKernel t ∘ₖ neutralKernel s

Uses 2 · Used by 5

Statement usesNeutral Wright–Fisher transition kernel at nonnegative time

Proof usesChapman–Kolmogorov equation for the Wright–Fisher diffusion

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

DefinitionCanonical path measure of the raw Wright–Fisher process#✓fully proved

The canonical probability measure on NNReal → I.

noncomputable def rawMeasure (x : I) : Measure SamplePath :=
  pathMeasure neutralKernel neutralKernel_add x

Uses 9 · Used by 9

Statement usesCanonical sample paths of the raw Wright–Fisher process · Neutral Wright–Fisher transition kernel at nonnegative time · Chapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Transition kernel of the neutral Wright–Fisher diffusion · Path-space measure of a Markov semigroup · Positive-operator-to-Markov-kernel bridge · Markov kernel of a positive unital operator

Used byContinuous realization of the raw Wright–Fisher process · Continuous 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 · Time-zero marginal of the raw path measure is the initial state · Two-time law of the raw Wright–Fisher path measure · Modified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws · Normalized raw process agrees with the coordinates almost surely

DefinitionRaw Wright–Fisher coordinate process#✓fully proved

The raw real-valued coordinate process, normalized at time zero on every sample rather than merely almost surely.

noncomputable def rawProcess (x : I) (t : NNReal) (ω : SamplePath) : ℝ :=
  if t = 0 then x else ω t

Uses 1 · Used by 6

Statement usesCanonical sample paths of the raw Wright–Fisher process

Used byContinuous realization of the raw Wright–Fisher process · Continuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process · Modified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws · Normalized raw process agrees with the coordinates almost surely

TheoremOne-time marginals of the raw Wright–Fisher path measure#✓fully proved

One-time marginals of the canonical raw path measure.

theorem map_eval_rawMeasure (x : I) (t : NNReal) :
    (rawMeasure x).map (fun ω => ω t) = neutralKernel t x

Uses 16 · Used by 1

Statement usesCanonical sample paths of the raw Wright–Fisher process · Neutral Wright–Fisher transition kernel at nonnegative time · Canonical path measure of the raw Wright–Fisher process

Proof usesChapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Transition kernel of the neutral Wright–Fisher diffusion · Finite-dimensional kernel of a Markov semigroup at ordered times · Finite-dimensional law of a Markov semigroup from a starting point · Restricting a finite Markov law along an increasing reindexing · Markov law at a finite set of times · Finite projections of the Markov path measure · Reindexing an ordered vector by a finite set · Path-space measure of a Markov semigroup · Positive-operator-to-Markov-kernel bridge · Markov kernel of a positive unital operator

Used byTime-zero marginal of the raw path measure is the initial state

TheoremTime-zero marginal of the raw path measure is the initial state#✓fully proved

The time-zero coordinate of the canonical path law is the prescribed initial state.

theorem map_eval_zero_rawMeasure (x : I) :
    (rawMeasure x).map (fun ω => ω 0) = Measure.dirac x

Uses 5 · Used by 1

Statement usesCanonical sample paths of the raw Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process

Proof usesOne-time marginals of the raw Wright–Fisher path measure · Neutral Wright–Fisher transition kernel at nonnegative time · Wright–Fisher transition kernel is the identity at time zero

Used byNormalized raw process agrees with the coordinates almost surely

TheoremTwo-time law of the raw Wright–Fisher path measure#✓fully proved

The ordered two-time law is the first marginal followed by the transition over the time gap.

theorem map_pair_rawMeasure_of_lt (x : I) {s t : NNReal} (hst : s < t) :
    (rawMeasure x).map (fun ω => (ω s, ω t)) =
      (neutralKernel s x) ⊗ₘ neutralKernel (t - s)

Uses 16 · Used by 1

Statement usesCanonical sample paths of the raw Wright–Fisher process · Neutral Wright–Fisher transition kernel at nonnegative time · Canonical path measure of the raw Wright–Fisher process

Proof usesChapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Transition kernel of the neutral Wright–Fisher diffusion · Finite-dimensional kernel of a Markov semigroup at ordered times · Finite-dimensional law of a Markov semigroup from a starting point · Restricting a finite Markov law along an increasing reindexing · Markov law at a finite set of times · Finite projections of the Markov path measure · Reindexing an ordered vector by a finite set · Path-space measure of a Markov semigroup · Positive-operator-to-Markov-kernel bridge · Markov kernel of a positive unital operator

Used byKolmogorov continuity condition for the raw Wright–Fisher process

TheoremNormalized raw process agrees with the coordinates almost surely#✓fully proved

Exact normalization changes no fixed-time law.

theorem rawProcess_ae_eq_coordinate (x : I) (t : NNReal) :
    rawProcess x t =ᵐ[rawMeasure x] fun ω => ((ω t : I) : ℝ)

Uses 4 · Used by 2

Statement usesCanonical sample paths of the raw Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process

Proof usesTime-zero marginal of the raw path measure is the initial state

Used byKolmogorov continuity condition for the raw Wright–Fisher process · Modified process has the canonical coordinate laws

DefinitionKolmogorov constant for the Wright–Fisher continuity bound#✓fully proved

The explicit Kolmogorov constant 3/16.

def kolmogorovConstant : NNReal := ⟨3 / 16, by positivity⟩

Used by 2

Used byContinuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process

TheoremKolmogorov continuity condition for the raw Wright–Fisher process#✓fully proved

The normalized raw coordinate process satisfies the explicit fourth-moment Kolmogorov condition with p=4, q=2, and M=3/16.

theorem isKolmogorovProcess_rawProcess (x : I) :
    IsKolmogorovProcess (rawProcess x) (rawMeasure x) 4 2
      kolmogorovConstant

Uses 22 · Used by 1

Statement usesCanonical sample paths of the raw Wright–Fisher process · Kolmogorov constant for the Wright–Fisher continuity bound · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process

Proof usesTwo-time law of the raw Wright–Fisher path measure · Neutral Wright–Fisher transition kernel at nonnegative time · Chapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Normalized raw process agrees with the coordinates almost surely · Wright–Fisher transition kernel represents the semigroup · Neutral Wright–Fisher diffusion semigroup · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Fourth-moment Kolmogorov bound for the Wright–Fisher semigroup · Transition kernel of the neutral Wright–Fisher diffusion · Finite-dimensional kernel of a Markov semigroup at ordered times · Finite-dimensional law of a Markov semigroup from a starting point · Markov law at a finite set of times · Path measure is the projective limit of the finite Markov laws · Reindexing an ordered vector by a finite set · Path-space measure of a Markov semigroup · Positive-operator-to-Markov-kernel bridge · Markov kernel of a positive unital operator

Used byContinuous modification selected by Kolmogorov's theorem

StructureContinuous realization of the raw Wright–Fisher process#✓fully proved

A selected continuous modification of the raw Wright--Fisher process, with all pathwise properties stated on every sample.

structure ContinuousRealization (x : I) where
  /-- The modified real-valued process. -/
  process : NNReal → SamplePath → ℝ
  /-- Every time coordinate is measurable. -/
  measurable : ∀ t, Measurable (process t)
  /-- Every sample path is continuous. -/
  continuous : ∀ ω, Continuous fun t => process t ω
  /-- Fixed-time almost-everywhere agreement with the normalized raw process. -/
  ae_eq_raw : ∀ t, process t =ᵐ[rawMeasure x] rawProcess x t
  /-- The initial value is exact on every sample. -/
  initial : ∀ ω, process 0 ω = x
  /-- Every value lies in the allele-frequency interval. -/
  mem_Icc : ∀ t ω, process t ω ∈ Set.Icc (0 : ℝ) 1

Uses 3 · Used by 4

Statement usesCanonical sample paths of the raw Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process

Used byContinuous modification selected by Kolmogorov's theorem · Modified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws · Continuous modified Wright–Fisher process

DefinitionContinuous modification selected by Kolmogorov's theorem#✓fully proved

The continuous modification selected by Kolmogorov's theorem.

noncomputable def continuousRealization (x : I) : ContinuousRealization x := by
  let h := exists_continuous_modification
    (isKolmogorovProcess_rawProcess x) (by norm_num : (1 : ℝ) < 2)
  let Y := Classical.choose h
  have hY := Classical.choose_spec h
  refine ⟨Y, hY.1, hY.2.1, hY.2.2.1, ?_, ?_⟩
  · intro ω
    change Classical.choose h 0 ω = (x : ℝ)
    rw [hY.2.2.2.1, rawProcess_zero]
  · intro t ω
    change Classical.choose h t ω ∈ Set.Icc (0 : ℝ) 1
    exact hY.2.2.2.2 (Set.Icc (0 : ℝ) 1) isClosed_Icc ω
      (fun s => rawProcess_mem_Icc x s ω) t

Uses 20 · Used by 3

Statement usesContinuous realization of the raw Wright–Fisher process · Canonical sample paths of the raw Wright–Fisher process · Kolmogorov continuity condition for the raw Wright–Fisher process · Kolmogorov constant for the Wright–Fisher continuity bound · Neutral Wright–Fisher transition kernel at nonnegative time · Chapman–Kolmogorov for the nonnegative-time Wright–Fisher kernel · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process · Wright–Fisher semigroup as a positive operator · Positive Wright–Fisher operator fixes constants · Transition kernel of the neutral Wright–Fisher diffusion · Kolmogorov continuous-modification theorem for real-valued processes · Finite-dimensional kernel of a Markov semigroup at ordered times · Finite-dimensional law of a Markov semigroup from a starting point · Markov law at a finite set of times · Path measure is the projective limit of the finite Markov laws · Reindexing an ordered vector by a finite set · Path-space measure of a Markov semigroup · Positive-operator-to-Markov-kernel bridge · Markov kernel of a positive unital operator

Used byModified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws · Continuous modified Wright–Fisher process

DefinitionContinuous modified Wright–Fisher process#✓fully proved

The concrete continuous process used by the final realization.

noncomputable def modifiedProcess (x : I) : NNReal → SamplePath → ℝ :=
  (continuousRealization x).process

Uses 3 · Used by 2

Statement usesContinuous realization of the raw Wright–Fisher process · Canonical sample paths of the raw Wright–Fisher process · Continuous modification selected by Kolmogorov's theorem

Used byModified process has the canonical coordinate laws · Modified process has the raw finite-dimensional laws

TheoremModified process has the raw finite-dimensional laws#✓fully proved

The modified process has the raw finite-dimensional laws, proved on each finite set by intersecting its fixed-time modification events.

theorem map_restrict_modified_eq_raw (x : I) (J : Finset NNReal) :
    (rawMeasure x).map
        (fun ω => J.restrict (fun t => modifiedProcess x t ω)) =
      (rawMeasure x).map
        (fun ω => J.restrict (fun t => rawProcess x t ω))

Uses 6

Statement usesCanonical sample paths of the raw Wright–Fisher process · Continuous modified Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process · Raw Wright–Fisher coordinate process

Proof usesContinuous realization of the raw Wright–Fisher process · Continuous modification selected by Kolmogorov's theorem

TheoremModified process has the canonical coordinate laws#✓fully proved

The modified finite-dimensional laws also equal the original canonical coordinate laws after coercion from I to ℝ.

theorem map_restrict_modified_eq_coordinate (x : I) (J : Finset NNReal) :
    (rawMeasure x).map
        (fun ω => J.restrict (fun t => modifiedProcess x t ω)) =
      (rawMeasure x).map
        (fun ω => J.restrict (fun t => ((ω t : I) : ℝ)))

Uses 7

Statement usesCanonical sample paths of the raw Wright–Fisher process · Continuous modified Wright–Fisher process · Canonical path measure of the raw Wright–Fisher process

Proof usesContinuous realization of the raw Wright–Fisher process · Continuous modification selected by Kolmogorov's theorem · Raw Wright–Fisher coordinate process · Normalized raw process agrees with the coordinates almost surely

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.