Ergodic

📁 Source: Mathlib/Dynamics/Ergodic/Ergodic.lean

Statistics

Metric	Count
Definitions Ergodic, PreErgodic, QuasiErgodic	3
Theorems ae_empty_or_univ_of_ae_le_preimage, ae_empty_or_univ_of_ae_le_preimage', ae_empty_or_univ_of_image_ae_le, ae_empty_or_univ_of_image_ae_le', ae_empty_or_univ_of_preimage_ae_le, ae_empty_or_univ_of_preimage_ae_le', quasiErgodic, smul_measure, symm_iff, toMeasurePreserving, toPreErgodic, zero_measure, ergodic_conjugate_iff, ergodic_of_ergodic_semiconj, preErgodic_conjugate_iff, preErgodic_of_preErgodic_conjugate, preErgodic_of_preErgodic_semiconj, ae_empty_or_univ, ae_mem_or_ae_notMem, aeconst_set, measure_self_or_compl_eq_zero, of_iterate, prob_eq_zero_or_one, smul_measure, zero_measure, ae_empty_or_univ₀, ae_mem_or_ae_notMem₀, aeconst_set₀, smul_measure, toPreErgodic, toQuasiMeasurePreserving, zero_measure	32
Total	35

Ergodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_empty_or_univ_of_ae_le_preimage 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass ae_empty_or_univ_of_ae_le_preimage' MeasureTheory.measure_ne_top
ae_empty_or_univ_of_ae_le_preimage' 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasurePreserving.measure_preimage toMeasurePreserving QuasiErgodic.ae_empty_or_univ₀ quasiErgodic Filter.EventuallyEq.symm MeasureTheory.ae_eq_of_ae_subset_of_measure_ge Eq.le
ae_empty_or_univ_of_image_ae_le 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.image	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass ae_empty_or_univ_of_image_ae_le' MeasureTheory.measure_ne_top
ae_empty_or_univ_of_image_ae_le' 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.image	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyLE.trans HasSubset.Subset.eventuallyLE Set.subset_preimage_image MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae MeasureTheory.MeasurePreserving.quasiMeasurePreserving toMeasurePreserving ae_empty_or_univ_of_ae_le_preimage'
ae_empty_or_univ_of_preimage_ae_le 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass ae_empty_or_univ_of_preimage_ae_le' MeasureTheory.measure_ne_top
ae_empty_or_univ_of_preimage_ae_le' 📖	mathematical	Ergodic MeasureTheory.NullMeasurableSet Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass QuasiErgodic.ae_empty_or_univ₀ quasiErgodic MeasureTheory.ae_eq_of_ae_subset_of_measure_ge Eq.ge MeasureTheory.MeasurePreserving.measure_preimage toMeasurePreserving MeasureTheory.NullMeasurableSet.preimage MeasureTheory.MeasurePreserving.quasiMeasurePreserving
quasiErgodic 📖	mathematical	Ergodic	QuasiErgodic	—	toPreErgodic MeasureTheory.MeasurePreserving.quasiMeasurePreserving toMeasurePreserving
smul_measure 📖	mathematical	Ergodic	MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	MeasureTheory.MeasurePreserving.smul_measure toMeasurePreserving PreErgodic.smul_measure toPreErgodic
symm_iff 📖	mathematical	—	Ergodic DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm	—	symm
toMeasurePreserving 📖	mathematical	Ergodic	MeasureTheory.MeasurePreserving	—	—
toPreErgodic 📖	mathematical	Ergodic	PreErgodic	—	—
zero_measure 📖	mathematical	Measurable	Ergodic MeasureTheory.Measure MeasureTheory.Measure.instZero	—	PreErgodic.zero_measure MeasureTheory.Measure.map_zero

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ergodic_conjugate_iff 📖	mathematical	MeasureTheory.MeasurePreserving DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike	Ergodic MeasurableEquiv.symm	—	comp_left_iff comp_right_iff symm preErgodic_conjugate_iff Ergodic.toMeasurePreserving Ergodic.toPreErgodic
ergodic_of_ergodic_semiconj 📖	—	MeasureTheory.MeasurePreserving Ergodic Measurable Function.Semiconj	—	—	of_semiconj Ergodic.toMeasurePreserving preErgodic_of_preErgodic_semiconj Ergodic.toPreErgodic
preErgodic_conjugate_iff 📖	mathematical	MeasureTheory.MeasurePreserving DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike	PreErgodic MeasurableEquiv.symm	—	preErgodic_of_preErgodic_semiconj symm MeasurableEquiv.symm_apply_apply
preErgodic_of_preErgodic_conjugate 📖	—	MeasureTheory.MeasurePreserving PreErgodic Function.Semiconj	—	—	preErgodic_of_preErgodic_semiconj
preErgodic_of_preErgodic_semiconj 📖	—	MeasureTheory.MeasurePreserving PreErgodic Function.Semiconj	—	—	MeasureTheory.Measure.instOuterMeasureClass aeconst_preimage MeasurableSet.nullMeasurableSet PreErgodic.aeconst_set measurable Set.preimage_comp Function.Semiconj.comp_eq

PreErgodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_empty_or_univ 📖	mathematical	PreErgodic MeasurableSet Set.preimage	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass aeconst_set
ae_mem_or_ae_notMem 📖	mathematical	PreErgodic MeasurableSet Set.preimage	Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyConst_set aeconst_set
aeconst_set 📖	mathematical	PreErgodic MeasurableSet Set.preimage	Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—
measure_self_or_compl_eq_zero 📖	mathematical	PreErgodic MeasurableSet Set.preimage	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal Compl.compl Set.instCompl	—	MeasureTheory.Measure.instOuterMeasureClass ae_empty_or_univ
of_iterate 📖	—	PreErgodic Nat.iterate	—	—	aeconst_set Function.IsFixedPt.preimage_iterate
prob_eq_zero_or_one 📖	mathematical	PreErgodic MeasurableSet Set.preimage	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	measure_self_or_compl_eq_zero
smul_measure 📖	mathematical	PreErgodic	MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	Filter.EventuallyConst.anti MeasureTheory.Measure.instOuterMeasureClass aeconst_set MeasureTheory.Measure.ae_smul_measure_le
zero_measure 📖	mathematical	—	PreErgodic MeasureTheory.Measure MeasureTheory.Measure.instZero	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_zero

QuasiErgodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_empty_or_univ₀ 📖	mathematical	QuasiErgodic MeasureTheory.NullMeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Set Set.instEmptyCollection Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyConst_set' aeconst_set₀
ae_mem_or_ae_notMem₀ 📖	mathematical	QuasiErgodic MeasureTheory.NullMeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.Eventually Set Set.instMembership	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyConst_set aeconst_set₀
aeconst_set₀ 📖	mathematical	QuasiErgodic MeasureTheory.NullMeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyConst	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae toQuasiMeasurePreserving Filter.EventuallyConst.congr PreErgodic.aeconst_set toPreErgodic
smul_measure 📖	mathematical	QuasiErgodic	MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure toQuasiMeasurePreserving PreErgodic.smul_measure toPreErgodic
toPreErgodic 📖	mathematical	QuasiErgodic	PreErgodic	—	—
toQuasiMeasurePreserving 📖	mathematical	QuasiErgodic	MeasureTheory.Measure.QuasiMeasurePreserving	—	—
zero_measure 📖	mathematical	Measurable	QuasiErgodic MeasureTheory.Measure MeasureTheory.Measure.instZero	—	PreErgodic.zero_measure MeasureTheory.Measure.map_zero

(root)

Definitions

Name	Category	Theorems
Ergodic 📖	CompData	26 math math: Ergodic.zero_measure, AddCircle.ergodic_nsmul_add, ergodic_mul_left_of_denseRange_pow, Ergodic.iff_mem_extremePoints_measure_univ_eq, AddCircle.ergodic_add_left, AddCircle.ergodic_add_right, ergodic_mul_left_iff_denseRange_zpow, ergodic_smul_of_denseRange_pow, AddCircle.ergodic_nsmul, ergodic_add_left_of_denseRange_zsmul, ergodic_vadd_of_denseRange_nsmul, AddCircle.ergodic_zsmul, ergodic_smul_of_denseRange_zpow, MeasureTheory.ergodicSMul_iterateMulAct, ergodic_mul_left_of_denseRange_zpow, ergodic_vadd_of_denseRange_zsmul, Ergodic.iff_mem_extremePoints, MeasureTheory.MeasurePreserving.ergodic_conjugate_iff, Ergodic.of_mem_extremePoints_measure_univ_eq, ergodic_add_left_iff_denseRange_zsmul, ergodic_add_left_of_denseRange_nsmul, Ergodic.symm_iff, AddMonoidHom.ergodic_of_dense_iUnion_preimage_zero, MonoidHom.ergodic_of_dense_iUnion_preimage_one, Ergodic.of_mem_extremePoints, AddCircle.ergodic_zsmul_add
PreErgodic 📖	CompData	6 math math: MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff, AddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero, MonoidHom.preErgodic_of_dense_iUnion_preimage_one, QuasiErgodic.toPreErgodic, Ergodic.toPreErgodic, PreErgodic.zero_measure
QuasiErgodic 📖	CompData	2 math math: Ergodic.quasiErgodic, QuasiErgodic.zero_measure

---

← Back to Index