Lean: E[Φ(first k steps)·Ψ(steps after k)] = E Φ · E Ψ for iid sequences

Pattern for renewal or strong-Markov-type factorizations of an iid sequence ξ : ℕ → Ω → ℝ without stopping-time machinery. Past σ-algebra: ⨆ j ∈ Set.Iio k, comap (ξ j). Future: ⨆ j ∈ Set.Ici k. Get Indep from indep_iSup_of_disjoint applied to (iIndepFun_iff_iIndep _ _ _).1 hind. Make the past functional measurable by composing with trunc k x := fun i ↦ if i < k then x i else 0, proved with @Measurable.of_eval Ω ℕ (fun _ ↦ ℝ) (past σ-alg) _ _ fun i ↦ ... (split_ifs; comap_measurable.mono (le_iSup₂ ...)). Then rw [IndepFun_iff_Indep] and use indep_of_indep_of_le_left/right with hX.comap_le. Then IndepFun.integral_fun_mul_eq_mul_integral needs only AEStronglyMeasurable, no integrability. Finally, the shifted sequence has the law of ξ: P.map (fun ω k ↦ ξ (σ k) ω) = P.map ξ for injective σ, via iIndepFun.map_fun_eq_infinitePi_map on both sides. To use this you must show your path functional is truncation invariant, e.g. psum (trunc k x) j = psum x j for j ≤ k.