Commit 2025-08-18 01:29 d77f47fd

feat(Dynamics/BirkhoffSum): add 2 lemmas for birkhoffSum/birkhoffAverage concerning ae_eq observables (#26074) If two observables are ae_eq then the birkhoffSum/birkhoffAverage of those observables are ae_eq. Motivation:

• Generally it is useful to be able to swap to observables which are ae_eq.
• Specifically this is useful to prove Birkhoff's pointwise ergodic theorem by first proving the result for integrable and measurable observables and then using this to deduce the result with just the requirement of integrable.