Basic

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

Statistics

Metric	Count
Definitions ErgodicSMul, ErgodicVAdd	2
Theorems aeconst_of_aestabilizer_eq_top, aeconst_of_forall_preimage_smul_ae_eq, of_aestabilizer, toSMulInvariantMeasure, aeconst_of_forall_preimage_vadd_ae_eq, toVAddInvariantMeasure, aeconst_of_forall_preimage_smul_ae_eq, aeconst_of_forall_preimage_vadd_ae_eq, aeconst_of_forall_smul_ae_eq, aeconst_of_forall_vadd_ae_eq, ergodicSMul_iterateMulAct, aeconst_of_aestabilizer_eq_top, ergodicSMul_iff, ergodicVAdd_iff	14
Total	16

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeconst_of_aestabilizer_eq_top 📖	mathematical	MeasureTheory.NullMeasurableSet aestabilizer ErgodicVAdd.toVAddInvariantMeasure AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction Top.top AddSubgroup AddSubgroup.instTop	Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ErgodicVAdd.toVAddInvariantMeasure MeasureTheory.aeconst_of_forall_vadd_ae_eq AddSubgroup.eq_top_iff'

ErgodicSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeconst_of_forall_preimage_smul_ae_eq 📖	mathematical	MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyConst	—	—
of_aestabilizer 📖	mathematical	Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ErgodicSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	MeasureTheory.Measure.instOuterMeasureClass Subgroup.eq_top_iff' Set.preimage_smul_inv
toSMulInvariantMeasure 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure	—	—

ErgodicVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeconst_of_forall_preimage_vadd_ae_eq 📖	mathematical	MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage HVAdd.hVAdd instHVAdd	Filter.EventuallyConst	—	—
toVAddInvariantMeasure 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeconst_of_forall_preimage_smul_ae_eq 📖	mathematical	NullMeasurableSet Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyConst	—	Measure.instOuterMeasureClass Filter.EventuallyConst.congr ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq Filter.EventuallyEq.trans tendsto_smul_ae ErgodicSMul.toSMulInvariantMeasure Filter.EventuallyEq.symm
aeconst_of_forall_preimage_vadd_ae_eq 📖	mathematical	NullMeasurableSet Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set.preimage HVAdd.hVAdd instHVAdd	Filter.EventuallyConst	—	Measure.instOuterMeasureClass Filter.EventuallyConst.congr ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq Filter.EventuallyEq.trans tendsto_vadd_ae ErgodicVAdd.toVAddInvariantMeasure Filter.EventuallyEq.symm
aeconst_of_forall_smul_ae_eq 📖	mathematical	NullMeasurableSet Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Filter.EventuallyConst	—	Measure.instOuterMeasureClass aeconst_of_forall_preimage_smul_ae_eq Set.preimage_smul
aeconst_of_forall_vadd_ae_eq 📖	mathematical	NullMeasurableSet Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	Filter.EventuallyConst	—	Measure.instOuterMeasureClass aeconst_of_forall_preimage_vadd_ae_eq Set.preimage_vadd
ergodicSMul_iterateMulAct 📖	mathematical	Measurable	ErgodicSMul IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction Ergodic	—	Measure.instOuterMeasureClass Function.IsFixedPt.preimage_iterate Filter.EventuallyEq.refl Ergodic.toMeasurePreserving QuasiErgodic.aeconst_set₀ Ergodic.quasiErgodic MeasurableSet.nullMeasurableSet

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeconst_of_aestabilizer_eq_top 📖	mathematical	MeasureTheory.NullMeasurableSet aestabilizer ErgodicSMul.toSMulInvariantMeasure SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction Top.top Subgroup Subgroup.instTop	Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ErgodicSMul.toSMulInvariantMeasure MeasureTheory.aeconst_of_forall_smul_ae_eq Subgroup.eq_top_iff'

(root)

Definitions

Name	Category	Theorems
ErgodicSMul 📖	CompData	6 math math: ErgodicSMul.of_aestabilizer, ergodicSMul_iff, ErgodicSMul.trans_isMinimal, MeasureTheory.ergodicSMul_iterateMulAct, instErgodicSMulMulOppositeOfIsMulRightInvariant, instErgodicSMulOfIsMulLeftInvariant
ErgodicVAdd 📖	CompData	4 math math: instErgodicVAddAddOppositeOfIsAddRightInvariant, ErgodicVAdd.trans_isMinimal, instErgodicVAddOfIsAddLeftInvariant, ergodicVAdd_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ergodicSMul_iff 📖	mathematical	—	ErgodicSMul MeasureTheory.SMulInvariantMeasure Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
ergodicVAdd_iff 📖	mathematical	—	ErgodicVAdd MeasureTheory.VAddInvariantMeasure Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass

---

← Back to Index