Markov processes from transition semigroups

DefinitionFinite-dimensional kernel of a Markov semigroup at ordered times#✓fully proved

The law, as a kernel in its starting point, at finitely many ordered times. s is the time of the input state and t lists the requested absolute times.

noncomputable def finiteChainKernel (K : NNReal → Kernel E E) (s : NNReal) :
    {n : ℕ} → (Fin n → NNReal) → Kernel E (Fin n → E)
  | 0, _ => Kernel.deterministic (fun _ i => Fin.elim0 i) (by fun_prop)
  | n + 1, t =>
      (K (t 0 - s) ⊗ₖ Kernel.prodMkLeft E
        (finiteChainKernel K (t 0) (fun i => t i.succ))).map
        (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) => E) 0).symm

Used by 11

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 · Kolmogorov extension for Markov semigroup laws · Composition rule for finite-chain kernels · Deleting the first time from a finite Markov chain kernel · Deleting one time from a finite Markov chain kernel · Restricting a finite Markov kernel along an increasing reindexing · Finite-dimensional law of a Markov semigroup from a starting point · Restricting a finite Markov law along an increasing reindexing

DefinitionFinite-dimensional law of a Markov semigroup from a starting point#✓fully proved

The ordered finite-dimensional law started from x at time s.

noncomputable def finiteChainLaw (K : NNReal → Kernel E E) (x : E)
    (s : NNReal) {n : ℕ} (t : Fin n → NNReal) : Measure (Fin n → E) :=
  finiteChainKernel K s t x

Uses 1 · Used by 9

Statement usesFinite-dimensional kernel of a Markov semigroup at ordered times

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 · Kolmogorov extension for Markov semigroup laws · Restricting a finite Markov law along an increasing reindexing · Markov law at a finite set of times · Finite Markov laws form a projective family · Ordered finite projections of the Markov path measure

TheoremComposition rule for finite-chain kernels#✓fully proved

Moving the starting time forward and then evolving to the first requested time gives the same finite chain as evolving there directly.

theorem finiteChainKernel_comp (K : NNReal → Kernel E E)
    [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    {s u : NNReal} (hsu : s ≤ u) {n : ℕ} (t : Fin n → NNReal)
    (hut : ∀ i, u ≤ t i) :
    finiteChainKernel K u t ∘ₖ K (u - s) = finiteChainKernel K s t

Uses 1 · Used by 1

Statement usesFinite-dimensional kernel of a Markov semigroup at ordered times

Used byDeleting the first time from a finite Markov chain kernel

DefinitionRemoving one coordinate from a finite vector#✓fully proved

Remove one coordinate from a finite vector.

def eraseCoordinate {n : ℕ} (j : Fin (n + 1)) :
    (Fin (n + 1) → E) → (Fin n → E) :=
  fun z i => z (j.succAbove i)

Used by 3

Used byDeleting the first time from a finite Markov chain kernel · Deleting one time from a finite Markov chain kernel · Restricting a finite Markov kernel along an increasing reindexing

TheoremDeleting the first time from a finite Markov chain kernel#✓fully proved

Deleting the first requested time composes the initial transition with the transition to the next requested time.

theorem finiteChainKernel_map_eraseCoordinate_zero
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    {s : NNReal} {n : ℕ} (t : Fin (n + 1) → NNReal)
    (hst : s ≤ t 0) (ht : StrictMono t) :
    (finiteChainKernel K s t).map
        (eraseCoordinate (E := E) (0 : Fin (n + 1))) =
      finiteChainKernel K s (fun i => t i.succ)

Uses 3 · Used by 1

Statement usesRemoving one coordinate from a finite vector · Finite-dimensional kernel of a Markov semigroup at ordered times

Proof usesComposition rule for finite-chain kernels

Used byDeleting one time from a finite Markov chain kernel

TheoremDeleting one time from a finite Markov chain kernel#✓fully proved

Deleting one requested time from an ordered finite Markov chain composes the two adjacent transition kernels.

theorem finiteChainKernel_map_eraseCoordinate
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    {s : NNReal} {n : ℕ} (t : Fin (n + 1) → NNReal)
    (hst : s ≤ t 0) (ht : StrictMono t) (j : Fin (n + 1)) :
    (finiteChainKernel K s t).map (eraseCoordinate (E := E) j) =
      finiteChainKernel K s (fun i => t (j.succAbove i))

Uses 3 · Used by 1

Statement usesRemoving one coordinate from a finite vector · Finite-dimensional kernel of a Markov semigroup at ordered times

Proof usesDeleting the first time from a finite Markov chain kernel

Used byRestricting a finite Markov kernel along an increasing reindexing

TheoremRestricting a finite Markov kernel along an increasing reindexing#✓fully proved

Restrict an ordered finite Markov law along any strictly increasing map of coordinate sets.

theorem finiteChainKernel_map_strictMono
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    {s : NNReal} {m n : ℕ} (t : Fin n → NNReal)
    (hst : ∀ i, s ≤ t i) (ht : StrictMono t)
    (e : Fin m → Fin n) (he : StrictMono e) :
    (finiteChainKernel K s t).map (fun z i => z (e i)) =
      finiteChainKernel K s (fun i => t (e i))

Uses 3 · Used by 1

Statement usesFinite-dimensional kernel of a Markov semigroup at ordered times

Proof usesRemoving one coordinate from a finite vector · Deleting one time from a finite Markov chain kernel

Used byRestricting a finite Markov law along an increasing reindexing

TheoremRestricting a finite Markov law along an increasing reindexing#✓fully proved

Measure form of finiteChainKernel_map_strictMono.

theorem finiteChainLaw_map_strictMono
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    (x : E) {s : NNReal} {m n : ℕ} (t : Fin n → NNReal)
    (hst : ∀ i, s ≤ t i) (ht : StrictMono t)
    (e : Fin m → Fin n) (he : StrictMono e) :
    (finiteChainLaw K x s t).map (fun z i => z (e i)) =
      finiteChainLaw K x s (fun i => t (e i))

Uses 3 · Used by 3

Statement usesFinite-dimensional law of a Markov semigroup from a starting point

Proof usesFinite-dimensional kernel of a Markov semigroup at ordered times · Restricting a finite Markov kernel along an increasing reindexing

Used byOne-time marginals of the raw Wright–Fisher path measure · Two-time law of the raw Wright–Fisher path measure · Finite Markov laws form a projective family

DefinitionReindexing an ordered vector by a finite set#✓fully proved

Reindex an ordered vector by the increasing enumeration of a finset.

noncomputable def orderMeasurableEquiv (J : Finset NNReal) :
    (Fin J.card → E) ≃ᵐ (J → E) where
  toFun y j := y ((J.orderIsoOfFin rfl).symm j)
  invFun y i := y (J.orderIsoOfFin rfl i)
  left_inv y := by
    ext i
    simp
  right_inv y := by
    ext j
    simp
  measurable_toFun := Measurable.of_eval fun _ => measurable_pi_apply _
  measurable_invFun := Measurable.of_eval fun _ => measurable_pi_apply _

Used by 8

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 · Kolmogorov extension for Markov semigroup laws · Markov law at a finite set of times · Finite Markov laws form a projective family · Ordered finite projections of the Markov path measure

DefinitionIncreasing reindexing of a subset within a finite set#✓fully proved

The increasing reindexing of the elements of J among those of a larger finset I.

noncomputable def orderRestriction {I J : Finset NNReal} (hJI : J ⊆ I) :
    Fin J.card ↪o Fin I.card :=
  OrderEmbedding.ofStrictMono
    (fun j => (I.orderIsoOfFin rfl).symm
      ⟨J.orderEmbOfFin rfl j, hJI (J.orderEmbOfFin_mem rfl j)⟩)
    (fun _a _b hab => (I.orderIsoOfFin rfl).symm.strictMono
      ((J.orderEmbOfFin rfl).strictMono hab))

Used by 1

Used byFinite Markov laws form a projective family

DefinitionMarkov law at a finite set of times#✓fully proved

The canonical law at an arbitrary finite set of nonnegative times.

The generic construction does not assume K 0 = Kernel.id. Consequently, when zero is requested its marginal is K 0 x; callers that need a deterministic initial value prove the identity law for their kernel.

noncomputable def finiteLaw (K : NNReal → Kernel E E) (x : E)
    (J : Finset NNReal) : Measure (J → E) :=
  (finiteChainLaw K x 0 (J.orderEmbOfFin rfl)).map
    (orderMeasurableEquiv J)

Uses 2 · Used by 10

Statement usesFinite-dimensional law of a Markov semigroup from a starting point · Reindexing an ordered vector by a finite set

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 · Kolmogorov extension for Markov semigroup laws · Path measure is the projective limit of the finite Markov laws · Finite Markov laws form a projective family · Ordered finite projections of the Markov path measure · Finite projections of the Markov path measure · Path-space measure of a Markov semigroup

TheoremFinite Markov laws form a projective family#✓fully proved

The finite laws obtained by sorting requested times form a projective family; projectivity is a consequence of Chapman--Kolmogorov, not a premise.

theorem isProjectiveMeasureFamily_finiteLaw
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s) (x : E) :
    IsProjectiveMeasureFamily (α := fun _ : NNReal => E)
      (finiteLaw K x)

Uses 5 · Used by 1

Statement usesMarkov law at a finite set of times

Proof usesFinite-dimensional law of a Markov semigroup from a starting point · Restricting a finite Markov law along an increasing reindexing · Reindexing an ordered vector by a finite set · Increasing reindexing of a subset within a finite set

Used byKolmogorov extension for Markov semigroup laws

TheoremKolmogorov extension for Markov semigroup laws#✓fully proved

Kolmogorov extension applied to the proved finite Markov laws.

theorem exists_projectiveLimit
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s) (x : E) :
    ∃ P : Measure (NNReal → E),
      IsProjectiveLimit P (finiteLaw K x)

Uses 6 · Used by 2

Statement usesMarkov law at a finite set of times

Proof usesKolmogorov extension theorem · Finite-dimensional kernel of a Markov semigroup at ordered times · Finite-dimensional law of a Markov semigroup from a starting point · Finite Markov laws form a projective family · Reindexing an ordered vector by a finite set

Used byPath measure is the projective limit of the finite Markov laws · Path-space measure of a Markov semigroup

DefinitionPath-space measure of a Markov semigroup#✓fully proved

The canonical path-space measure selected from Kolmogorov extension.

As for finiteLaw, no identity-at-zero hypothesis is built into this generic object: its time-zero marginal is K 0 x unless the caller proves K 0 = Kernel.id.

noncomputable def pathMeasure
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s) (x : E) :
    Measure (NNReal → E) :=
  Classical.choose (exists_projectiveLimit K hKadd x)

Uses 2 · Used by 8

Statement usesKolmogorov extension for Markov semigroup laws · Markov law at a finite set of times

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 · Path measure is the projective limit of the finite Markov laws · Ordered finite projections of the Markov path measure · Finite projections of the Markov path measure

TheoremPath measure is the projective limit of the finite Markov laws#✓fully proved

The canonical path measure has exactly the constructed finite laws.

theorem isProjectiveLimit_pathMeasure
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s) (x : E) :
    IsProjectiveLimit (pathMeasure K hKadd x) (finiteLaw K x)

Uses 3 · Used by 3

Statement usesMarkov law at a finite set of times · Path-space measure of a Markov semigroup

Proof usesKolmogorov extension for Markov semigroup laws

Used byContinuous modification selected by Kolmogorov's theorem · Kolmogorov continuity condition for the raw Wright–Fisher process · Finite projections of the Markov path measure

TheoremFinite projections of the Markov path measure#✓fully proved

Every finite coordinate projection of the canonical path measure is its explicit iterated-kernel law.

theorem map_restrict_pathMeasure
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    (x : E) (J : Finset NNReal) :
    (pathMeasure K hKadd x).map J.restrict = finiteLaw K x J

Uses 3 · Used by 3

Statement usesMarkov law at a finite set of times · Path-space measure of a Markov semigroup

Proof usesPath measure is the projective limit of the finite Markov laws

Used byOne-time marginals of the raw Wright–Fisher path measure · Two-time law of the raw Wright–Fisher path measure · Ordered finite projections of the Markov path measure

TheoremOrdered finite projections of the Markov path measure#✓fully proved

The coordinates in increasing finset order have exactly the corresponding iterated-kernel law.

theorem map_ordered_pathMeasure
    (K : NNReal → Kernel E E) [∀ t, IsMarkovKernel (K t)]
    (hKadd : ∀ s t, K (s + t) = K t ∘ₖ K s)
    (x : E) (J : Finset NNReal) :
    (pathMeasure K hKadd x).map
        (fun ω i => ω (J.orderEmbOfFin rfl i)) =
      finiteChainLaw K x 0 (J.orderEmbOfFin rfl)

Uses 5

Statement usesFinite-dimensional law of a Markov semigroup from a starting point · Path-space measure of a Markov semigroup

Proof usesMarkov law at a finite set of times · Finite projections of the Markov path measure · Reindexing an ordered vector by a finite set

TheoremRepresentation of positive unital operators by Markov kernels#✓fully proved

A positive unital linear map from C(E, ℝ) to itself is represented by a Markov kernel. Continuity of the operator is unnecessary: each output already belongs to C(E, ℝ).

theorem exists_markovKernelOfPositiveLinearMap (T : C(E, ℝ) →ₚ[ℝ] C(E, ℝ))
    (hT : T 1 = 1) :
    ∃ K : Kernel E E, IsMarkovKernel K ∧
      ∀ (f : C(E, ℝ)) (x : E), ∫ y, f y ∂K x = T f x

Used by 1

Used byPositive-operator-to-Markov-kernel bridge

TheoremPositive-operator-to-Markov-kernel bridge#✓fully proved

On a compact metrizable Borel space, a positive continuous linear operator on C(E, ℝ) that fixes 1 is represented by a Markov kernel. The integral identity holds for every continuous function and every starting state.

theorem exists_markovKernelOfPositiveOperator (T : C(E, ℝ) →P[ℝ] C(E, ℝ))
    (hT : T 1 = 1) :
    ∃ K : Kernel E E, IsMarkovKernel K ∧
      ∀ (f : C(E, ℝ)) (x : E), ∫ y, f y ∂K x = T f x

Uses 1 · Used by 10

Proof usesRepresentation of positive unital operators by Markov kernels

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 is the identity at nonpositive times · Kernel of a positive operator represents it on continuous functions · Markov kernel of a positive unital operator · Operator composition corresponds to kernel composition · Identity operator gives the identity kernel

DefinitionMarkov kernel of a positive unital operator#✓fully proved

The canonical chosen Markov kernel representing T. Its characterization theorem is integral_markovKernelOfPositiveOperator; clients should use that theorem rather than unfold this definition.

noncomputable def markovKernelOfPositiveOperator (T : C(E, ℝ) →P[ℝ] C(E, ℝ))
    (hT : T 1 = 1) : Kernel E E :=
  (exists_markovKernelOfPositiveOperator T hT).choose

Uses 1 · Used by 13

Statement usesPositive-operator-to-Markov-kernel bridge

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 · Kernel of a positive operator represents it on continuous functions · Operator composition corresponds to kernel composition · Identity operator gives the identity kernel · Identity operator kernel is pointwise Dirac

TheoremKernel of a positive operator represents it on continuous functions#✓fully proved

The chosen kernel represents T on every real-valued continuous function.

@[simp]
theorem integral_markovKernelOfPositiveOperator (T : C(E, ℝ) →P[ℝ] C(E, ℝ))
    (hT : T 1 = 1) (f : C(E, ℝ)) (x : E) :
    ∫ y, f y ∂markovKernelOfPositiveOperator T hT x = T f x

Uses 2 · Used by 3

Statement usesMarkov kernel of a positive unital operator

Proof usesPositive-operator-to-Markov-kernel bridge

Used byWright–Fisher transition kernel represents the semigroup · Operator composition corresponds to kernel composition · Identity operator gives the identity kernel

TheoremMarkov kernels are determined by integrals of continuous functions#✓fully proved

Two Markov kernels on a compact metrizable Borel space are equal when they integrate every real-valued continuous function equally at every starting state.

theorem kernel_ext_of_forall_integral_continuous_eq {K L : Kernel E E}
    [IsMarkovKernel K] [IsMarkovKernel L]
    (h : ∀ (f : C(E, ℝ)) (x : E), ∫ y, f y ∂K x = ∫ y, f y ∂L x) : K = L

Used by 3

Used byWright–Fisher transition kernel is the identity at nonpositive times · Operator composition corresponds to kernel composition · Identity operator gives the identity kernel

TheoremIdentity operator gives the identity kernel#✓fully proved

The kernel represented by the identity operator is Mathlib's identity kernel.

theorem markovKernelOfPositiveOperator_id :
    markovKernelOfPositiveOperator (PositiveContinuousLinearMap.id ℝ C(E, ℝ)) (by rfl) =
      (Kernel.id : Kernel E E)

Uses 4 · Used by 1

Statement usesMarkov kernel of a positive unital operator

Proof usesPositive-operator-to-Markov-kernel bridge · Kernel of a positive operator represents it on continuous functions · Markov kernels are determined by integrals of continuous functions

Used byIdentity operator kernel is pointwise Dirac

TheoremIdentity operator kernel is pointwise Dirac#✓fully proved

Pointwise form of the identity theorem: every transition measure is Dirac.

@[simp]
theorem markovKernelOfPositiveOperator_id_apply (x : E) :
    markovKernelOfPositiveOperator (PositiveContinuousLinearMap.id ℝ C(E, ℝ)) (by rfl) x =
      Measure.dirac x

Uses 2

Statement usesMarkov kernel of a positive unital operator

Proof usesIdentity operator gives the identity kernel

TheoremOperator composition corresponds to kernel composition#✓fully proved

Operator composition is represented by canonical kernel composition. The order is reversed: T.comp U acts as f ↦ T (U f), so the represented kernel first uses K_T and then K_U.

theorem markovKernelOfPositiveOperator_comp (T U : C(E, ℝ) →P[ℝ] C(E, ℝ))
    (hT : T 1 = 1) (hU : U 1 = 1) :
    markovKernelOfPositiveOperator (T.comp U) (by
      change T (U 1) = 1
      rw [hU, hT]) =
      markovKernelOfPositiveOperator U hU ∘ₖ markovKernelOfPositiveOperator T hT

Uses 4 · Used by 1

Statement usesMarkov kernel of a positive unital operator

Proof usesPositive-operator-to-Markov-kernel bridge · Kernel of a positive operator represents it on continuous functions · Markov kernels are determined by integrals of continuous functions

Used byChapman–Kolmogorov equation for the Wright–Fisher diffusion

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.