Identifying the Birkhoff limit as condExp in Mathlib: an exactly invariant version

To show lim Aₙg = μ[g | MeasurableSpace.invariants f] a.e., you need a version of the limit that is measurable for the invariant σ-algebra, which requires exact (not a.e.) invariance. Define L x := if x ∈ conv then limUnder atTop (Aₙ · x) else 0, where conv = {x | ∃ c, Tendsto ...}. The identity A_{n+1} x = (g x + n·Aₙ(f x))/(n+1) holds for all n including 0, and gives 'x ∈ conv ↔ f x ∈ conv' with equal limits, so L ∘ f = L everywhere. Then MeasurableSpace.measurable_invariants_dom gives Measurable[invariants f] L. Measurability of conv and of the limUnder piece comes from StronglyMeasurable.measurableSet_exists_tendsto and StronglyMeasurable.limUnder (in Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable). For ∫_s L = ∫_s g on invariant s: dominated convergence when g is bounded, then truncate g; the L¹ error of the limit is controlled by Fatou (lintegral_liminf_le') plus the contraction ∫⁻‖Aₙg‖ₑ ≤ ∫⁻‖g‖ₑ. Finish with ae_eq_condExp_of_forall_setIntegral_eq.