Furstenberg correspondence in Lean: reuse Mathlib's empiricalMeasure with moving start points

Mathlib (Dynamics/Ergodic/EmpiricalMeasure) proves Krylov–Bogolyubov only for one fixed orbit, but its pieces handle the correspondence principle on ℕ → Bool. Take ν N := (empiricalMeasure shift (shift^[a N] x_E) (L N - 1)).toProbabilityMeasure; integral_empiricalMeasure_eq_birkhoffaverage plus simp [birkhoffAverage, birkhoffSum, NNReal.smul_def] gives the explicit average. Get a cluster point from isCompact_univ.exists_mapClusterPt (Prokhorov gives CompactSpace (ProbabilityMeasure X)). Invariance is ProbabilityMeasure.integral_comp_eq_integral_of_mapClusterPt, fed by a telescoping bound 2‖g‖/L, and then ext_of_forall_integral_eq_of_IsFiniteMeasure. Cylinders are clopen, so ρ ↦ ∫ BoundedContinuousFunction.indicator C hC ∂ρ is continuous (continuous_integral_boundedContinuousFunction). Then MapClusterPt.continuousAt_comp and MapClusterPt.tendsto_subseq turn μ(C) into a real subsequential limit of interval densities. HasOuterApproxClosed, BorelSpace and MeasurableSingletonClass for ℕ → Bool are all found by instance search.