Partial trajectories at the next time

Evaluating a partial trajectory from time a at time a + 1 recovers the step kernel κ a, however far the trajectory runs, and the one-step trajectory from x is the step kernel at x pushed forward by appending its value to x. In discrete state spaces this gives the chain rule partialTraj_succ_apply_singleton: the mass of a trajectory up to time b + 1 is the mass of its restriction to time b times the probability of its last step. [UPSTREAM] candidates for Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean.

theorem ProbabilityTheory.Kernel.map_partialTraj_eval_succ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {a b : ℕ} (hab : a + 1 ≤ b) : ((partialTraj κ a b).map fun (x : (i : ↥(Finset.Iic b)) → X ↑i) => x ⟨a + 1, ⋯⟩) = κ a

The pushforward of partialTraj κ a b along the point at time a + 1 is κ a.

theorem ProbabilityTheory.Kernel.partialTraj_succ_self_apply {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] (a : ℕ) (x : (i : ↥(Finset.Iic a)) → X ↑i) : (partialTraj κ a (a + 1)) x = MeasureTheory.Measure.map (fun (y : X (a + 1)) => IicProdIoc a (a + 1) (x, (MeasurableEquiv.piSingleton a) y)) ((κ a) x)

The one-step trajectory from x is κ a x pushed forward by appending its value to x.

theorem ProbabilityTheory.Kernel.IicProdIoc_piSingleton_eq_iff {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {b : ℕ} {z : (i : ↥(Finset.Iic b)) → X ↑i} {w : X (b + 1)} {y : (i : ↥(Finset.Iic (b + 1))) → X ↑i} : IicProdIoc b (b + 1) (z, (MeasurableEquiv.piSingleton b) w) = y ↔ z = Preorder.frestrictLe₂ ⋯ y ∧ w = y ⟨b + 1, ⋯⟩

A trajectory up to time b + 1 is obtained by appending exactly one point to exactly one trajectory up to time b.

theorem ProbabilityTheory.Kernel.partialTraj_succ_apply_singleton {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] [∀ (n : ℕ), Countable (X n)] [∀ (n : ℕ), MeasurableSingletonClass (X n)] {a b : ℕ} (hab : a ≤ b) (x : (i : ↥(Finset.Iic a)) → X ↑i) (y : (i : ↥(Finset.Iic (b + 1))) → X ↑i) : ((partialTraj κ a (b + 1)) x) {y} = ((partialTraj κ a b) x) {Preorder.frestrictLe₂ ⋯ y} * ((κ b) (Preorder.frestrictLe₂ ⋯ y)) {y ⟨b + 1, ⋯⟩}

In discrete state spaces, the mass of a trajectory up to time b + 1 is the mass of its restriction to time b times the probability of its last step.