QuasiMeasurePreserving

📁 Source: Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean

Statistics

Metric	Count
Definitions	0
Theorems birkhoffAverage_ae_eq_of_ae_eq, birkhoffSum_ae_eq_of_ae_eq	2
Total	2

MeasureTheory.Measure.QuasiMeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
birkhoffAverage_ae_eq_of_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	birkhoffAverage	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.const_smul birkhoffSum_ae_eq_of_ae_eq
birkhoffSum_ae_eq_of_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	birkhoffSum	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono MeasureTheory.ae_all_iff instCountableNat ae iterate Finset.sum_congr

---

← Back to Index