Faithfulness of the transition-operator expectation

expList α T F was defined by recursion (average out the first draw, then recurse). This file proves it equals the textbook object: the uniform average of F over all length-T sequences of draws, i.e. over the product probability space Fin T → α of T i.i.d. uniform rounds.

theorem Dynamics.expList_eq_avg_ofFn {α : Type u_1} [Fintype α] (T : ℕ) (F : List α → ℝ) : expList α T F = avg fun (ω : Fin T → α) => F (List.ofFn ω)