Concatenating finite-time kernels at an ordered cut

This file factors an ordered finite-dimensional transition law at a designated observation time. The future factor is the finite-time kernel at the corresponding relative times, started from the terminal coordinate of the past. This is finite-dimensional kernel infrastructure and does not assert a path-space or conditional Markov theorem.

def MarkovProcess.cutIndexOrderIso (m n : ℕ) : Fin (m + 1 + n) ≃o Fin (n + (m + 1))

Reassociate the cardinality of a split finite path so recursion removes its first point definitionally while the coordinate order remains past-then-future.

Equations

• MarkovProcess.cutIndexOrderIso m n = Fin.castOrderIso ⋯

def MarkovProcess.FiniteOrderedTimes.initialSegment {m n : ℕ} (times : FiniteOrderedTimes (n + (m + 1))) : FiniteOrderedTimes (m + 1)

Restrict an ordered family to the coordinates at or before a designated cut.

Equations

• times.initialSegment = times.restrict (RelEmbedding.trans (Fin.castAddOrderEmb n) (MarkovProcess.cutIndexOrderIso m n).toOrderEmbedding)

def MarkovProcess.FiniteOrderedTimes.relativeFinalSegment {m n : ℕ} (times : FiniteOrderedTimes (n + (m + 1))) : FiniteOrderedTimes n

Times after the cut, measured relative to the time at the cut.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MarkovProcess.FiniteOrderedTimes.relativeFinalSegment_apply {m n : ℕ} (times : FiniteOrderedTimes (n + (m + 1))) (i : Fin n) : times.relativeFinalSegment i = times ((cutIndexOrderIso m n) (Fin.natAdd (m + 1) i)) - times ((cutIndexOrderIso m n) (Fin.castAdd n (Fin.last m)))

def MarkovProcess.SubMarkovKernelSemigroup.splitFinitePath {alpha : Type u_1} {m n : ℕ} (path : Fin (n + (m + 1)) → alpha) : (Fin (m + 1) → alpha) × (Fin n → alpha)

Separate a finite path into its coordinates at or before the cut and those after the cut.

Equations

• One or more equations did not get rendered due to their size.

theorem MarkovProcess.SubMarkovKernelSemigroup.measurable_splitFinitePath {alpha : Type u_1} [MeasurableSpace alpha] {m n : ℕ} : Measurable splitFinitePath

Splitting a finite path at a cut is measurable.

def MarkovProcess.SubMarkovKernelSemigroup.splitPastTerminal {alpha : Type u_1} {m : ℕ} (z : alpha × (Fin (m + 1) → alpha)) : alpha

The terminal state of the first component of a split finite path.

Equations

• MarkovProcess.SubMarkovKernelSemigroup.splitPastTerminal z = z.2 (Fin.last m)

theorem MarkovProcess.SubMarkovKernelSemigroup.measurable_splitPastTerminal {alpha : Type u_1} [MeasurableSpace alpha] {m : ℕ} : Measurable splitPastTerminal

Reading the terminal past coordinate is measurable.

def MarkovProcess.SubMarkovKernelSemigroup.finConsMeasurableEquiv {alpha : Type u_1} [MeasurableSpace alpha] (n : ℕ) : alpha × (Fin n → alpha) ≃ᵐ (Fin (n + 1) → alpha)

Measurable equivalence between a head/tail pair and a finite successor path.

Equations

• MarkovProcess.SubMarkovKernelSemigroup.finConsMeasurableEquiv n = (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => alpha) 0).symm

@[simp]

theorem MarkovProcess.SubMarkovKernelSemigroup.finConsMeasurableEquiv_apply {alpha : Type u_1} [MeasurableSpace alpha] (n : ℕ) (z : alpha × (Fin n → alpha)) : (finConsMeasurableEquiv n) z = Fin.cons z.1 z.2

@[simp]

theorem MarkovProcess.SubMarkovKernelSemigroup.finConsMeasurableEquiv_symm_apply {alpha : Type u_1} [MeasurableSpace alpha] (n : ℕ) (path : Fin (n + 1) → alpha) : (finConsMeasurableEquiv n).symm path = (path 0, Fin.tail path)

theorem MarkovProcess.SubMarkovKernelSemigroup.finiteTimeKernel_map_headTail {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {n : ℕ} (times : FiniteOrderedTimes (n + 1)) : ((P.finiteTimeKernel times).map fun (path : Fin (n + 1) → alpha) => (path 0, Fin.tail path)) = (P.kernel (times 0)).compProd (ProbabilityTheory.Kernel.prodMkLeft alpha (P.finiteTimeKernel times.relativeTail))

Splitting the finite-time kernel after its first observation recovers exactly the recursive transition-kernel product used in its construction.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.finiteTimeKernel_map_splitFinitePath {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (m n : ℕ) (times : FiniteOrderedTimes (n + (m + 1))) : (P.finiteTimeKernel times).map splitFinitePath = (P.finiteTimeKernel times.initialSegment).compProd ((P.finiteTimeKernel times.relativeFinalSegment).comap splitPastTerminal ⋯)

Splitting an ordered finite-dimensional law at a cut factors it into its past law and the relative future law started from the terminal state of that past.