Documentation

LeanPool.MarkovProcess.MarkovProcess.Feller.BackwardC0Recursion

Backward C₀ recursion for finite Feller transitions #

An ordered nonempty family of one-coordinate C₀ factors determines a backward semigroup recursion: evolve the last factors relative to the first time, multiply by the first factor, and then evolve from the starting state to the first time. The recursion varies continuously in the C₀ norm when every ordered observation time converges.

This file contains only the analytic recursion and its continuity. Its identification with an integral against a finite-time kernel is in Feller/BackwardC0Integral.lean; no statement about path space is proved here.

source
noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.backwardC0 {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) {n : ℕ} :
FiniteOrderedTimes (n + 1) → (Fin (n + 1) → ZeroAtInftyContinuousMap alpha ℝ) → ZeroAtInftyContinuousMap alpha ℝ

Backward semigroup recursion for a nonempty ordered family of coordinatewise C₀ factors.

Equations
Instances For
    source
    @[simp]
    theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.backwardC0_zero {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) (times : FiniteOrderedTimes 1) (factors : Fin 1 → ZeroAtInftyContinuousMap alpha ℝ) :
    hP.backwardC0 times factors = (hP.c0Semigroup.operator (times 0)) (factors 0)

    The backward recursion for a singleton family is one Feller-semigroup application.

    source
    @[simp]
    theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.backwardC0_succ {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) {n : ℕ} (times : FiniteOrderedTimes (n + 2)) (factors : Fin (n + 2) → ZeroAtInftyContinuousMap alpha ℝ) :
    hP.backwardC0 times factors = (hP.c0Semigroup.operator (times 0)) (factors 0 * hP.backwardC0 times.relativeTail (Fin.tail factors))

    At a successor length, the backward recursion multiplies the first factor by the recursively evolved relative tail before applying the first transition.

    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.tendsto_backwardC0 {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) {X : Type u_2} {l : Filter X} {n : ℕ} {times : X → FiniteOrderedTimes (n + 1)} {times0 : FiniteOrderedTimes (n + 1)} (ht : ∀ (i : Fin (n + 1)), Filter.Tendsto (fun (a : X) => (times a) i) l (nhds (times0 i))) (factors : Fin (n + 1) → ZeroAtInftyContinuousMap alpha ℝ) :
    Filter.Tendsto (fun (a : X) => hP.backwardC0 (times a) factors) l (nhds (hP.backwardC0 times0 factors))

    The backward recursion is continuous in the C₀ norm under coordinatewise convergence of a nonempty ordered time family.