Time reversal of i.i.d. rounds (roadmap FND-6)

The T rounds averaged by expList are i.i.d. uniform, so their joint law is invariant under reversing their order: expList α T (F ∘ List.reverse) = expList α T F. The proof goes through the product form expList_eq_avg_ofFn of Dynamics.Equivalence and the reindexing of Fin T → α by Fin.rev.

For a process driven by rounds, iterate_ofStep reads the rounds first to last (a left fold); by time reversal the same expectation is obtained by applying them last to first (a right fold), which is the form of backward (dual) processes such as coalescing random walks.

theorem Dynamics.reverse_ofFn {α : Type u_1} {n : ℕ} (ω : Fin n → α) : (List.ofFn ω).reverse = List.ofFn (ω ∘ Fin.rev)

Reversing a list of draws is precomposing the draws with Fin.rev.

theorem Dynamics.expList_comp_reverse {α : Type u_1} [Fintype α] (T : ℕ) (F : List α → ℝ) : expList α T (F ∘ List.reverse) = expList α T F

Time reversal of i.i.d. rounds (roadmap FND-6). Reversing the order of T i.i.d. uniform rounds does not change the expectation of any functional of them.

theorem Dynamics.Kernel.iterate_ofStep_foldr {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (T : ℕ) (f : S → ℝ) (s : S) : (ofStep step).iterate T f s = expList R T fun (l : List R) => f (List.foldr (fun (r : R) (t : S) => step t r) s l)

Time reversal for round-based kernels (roadmap FND-6). Iterating ofStep step is averaging over T i.i.d. rounds applied in reverse order, i.e. along the right fold.