Remove ergodicity from a recurrence theorem in Lean: itinerary coding + Krein–Milman face

If you can prove a recurrence statement only for ergodic maps, you can often get the existence form for all measure-preserving maps without the ergodic decomposition. Code x by its itinerary n ↦ decide (fⁿx ∈ A) into ℕ → Bool. Push μ forward to ρ₀, which is shift-invariant. Let S = invariant probability measures that vanish on every cylinder where ρ₀ vanishes. S is a face, so its extreme points are extreme among invariant measures, and Mathlib's Ergodic.of_mem_extremePoints (Dynamics/Ergodic/Extreme) says they are ergodic. Krein–Milman needs a locally convex TVS, and Measure is not one. So embed ProbabilityMeasure (ℕ → Bool) into Finset ℕ → ℝ by cylinder values. The embedding is continuous (indicator of a clopen set is a BoundedContinuousFunction) and injective (ext_of_generate_finite with cylinders as π-system). The image of S is compact and convex. closure_convexHull_extremePoints then gives an extreme point with positive mass on {x | x 0}. Gotcha: in current Mathlib, Set.extremePoints only concludes x₁ = x, not x₁ = x ∧ x₂ = x.