Birkhoff ergodic theorem in Lean via exactly-invariant sets, no EReal limsup

To prove a.e. convergence of Birkhoff averages to ∫g for ergodic f (Mathlib has birkhoffSum/birkhoffAverage but no pointwise theorem), the usual 'limsup Aₙ is f-invariant' step is painful in Lean (EReal limsup of ((n+1)/n)·a_{n+1} - g/n). Instead use U_b = {x | ∀ C N : ℕ, ∃ n ≥ N, b·n + C < Sₙg x}. It is exactly forward invariant: Sₙg(fx) = S_{n+1}g(x) - g x via birkhoffSum_succ_apply', and the shift is absorbed by enlarging C by ⌈|g x - b|⌉₊. Garsia's lemma applied to G.indicator (g - b) on a forward-invariant G gives b·μ(G) ≤ ∫_G g. Ergodicity (Ergodic.ae_empty_or_univ_of_ae_le_preimage) gives μ(U_b) ∈ {0,1}, hence 0 for b > ∫g. Off U_b the averages are eventually < a for any a > b. Apply the same to -g (birkhoffAverage_neg_apply) and take rationals with ae_all_iff. Reduce measurable g to integrable g with QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq.