📁 Source: Mathlib/Dynamics/Ergodic/AddCircle.lean
ae_empty_or_univ_of_forall_vadd_ae_eq_self
ergodic_nsmul
ergodic_nsmul_add
ergodic_zsmul
ergodic_zsmul_add
MeasureTheory.NullMeasurableSet
AddCircle
Real
Real.instAddCommGroup
MeasureTheory.MeasureSpace.toMeasurableSpace
measureSpace
MeasureTheory.MeasureSpace.volume
Filter.EventuallyEq
MeasureTheory.ae
MeasureTheory.Measure
MeasureTheory.Measure.instFunLike
MeasureTheory.Measure.instOuterMeasureClass
HVAdd.hVAdd
Set
instHVAdd
Set.vaddSet
AddSemigroupAction.toVAdd
AddMonoid.toAddSemigroup
ESeminormedAddMonoid.toAddMonoid
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
instNormedAddCommGroupReal
ESeminormedAddCommMonoid.toESeminormedAddMonoid
ENormedAddCommMonoid.toESeminormedAddCommMonoid
NormedAddCommGroup.toENormedAddCommMonoid
AddAction.toAddSemigroupAction
AddTorsor.toAddAction
QuotientAddGroup.Quotient.addGroup
AddCommGroup.toAddGroup
AddSubgroup.zmultiples
AddSubgroup.normal_of_comm
NormedAddTorsor.toAddTorsor
QuotientAddGroup.instSeminormedAddCommGroup
NonUnitalSeminormedRing.toSeminormedAddCommGroup
NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing
SeminormedCommRing.toNonUnitalSeminormedCommRing
NormedCommRing.toSeminormedCommRing
Real.normedCommRing
SeminormedAddCommGroup.toNormedAddTorsor
Filter.Tendsto
addOrderOf
Filter.atTop
Nat.instPreorder
Set.instEmptyCollection
Set.univ
Fact.out
MeasureTheory.ae_eq_empty
MeasureTheory.ae_eq_univ_iff_measure_eq
isFiniteMeasure
measure_univ
eq_or_ne
MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae
IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div
instIsUnifLocDoublingMeasureRealVolume
QuotientAddGroup.instSecondCountableTopology
IsTopologicalSemiring.toContinuousAdd
IsTopologicalRing.toIsTopologicalSemiring
instIsTopologicalRingReal
instSecondCountableTopologyReal
QuotientAddGroup.borelSpace
instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace
TopologicalSpace.SecondCountableTopology.to_separableSpace
TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable
Real.instCompleteSpace
EMetric.instIsCountablyGeneratedUniformity
T6Space.toT0Space
instT6SpaceOfMetrizableSpace
EMetricSpace.metrizableSpace
instIsTopologicalAddGroupReal
Real.borelSpace
AddSubgroup.isClosed_of_discrete
TopologicalSpace.t2Space_of_metrizableSpace
Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples
MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts
instWeaklyLocallyCompactSpaceOfLocallyCompactSpace
QuotientAddGroup.instLocallyCompactSpace
locallyCompact_of_proper
instProperSpaceReal
MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts
instIsAddHaarMeasureRealVolume
Nat.instAtLeastTwoHAddOfNat
Filter.Eventually.mono
Filter.Tendsto.eventually_gt_atTop
instNoTopOrderOfNoMaxOrder
Nat.instNoMaxOrder
div_pos
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
Real.instIsStrictOrderedRing
mul_pos
Mathlib.Meta.Positivity.pos_of_isNat
Real.instIsOrderedRing
Real.instNontrivial
Mathlib.Meta.NormNum.isNat_ofNat
Mathlib.Meta.NormNum.instAtLeastTwo
Nat.cast_pos'
IsOrderedAddMonoid.toAddLeftMono
Real.instIsOrderedAddMonoid
Real.instZeroLEOneClass
NeZero.charZero_one
RCLike.charZero_rclike
tendsto_nhdsWithin_iff
Filter.Tendsto.const_mul_atTop
inv_pos_of_pos
tendsto_natCast_atTop_iff
Real.instArchimedean
div_eq_inv_mul
mul_inv_rev
inv_inv
Filter.Tendsto.inv_tendsto_atTop
instOrderTopologyReal
one_mul
dist_self
LT.lt.le
addOrderOf_pos_iff
Nat.cast_one
LT.lt.ne
Metric.measure_closedBall_pos
MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure
MeasureTheory.measure_ne_top
volume_closedBall
mul_div
mul_div_mul_left
two_ne_zero
CharZero.NeZero.two
min_eq_right
div_le_self
mul_comm
nsmul_eq_mul
ENNReal.ofReal_nsmul
mul_div_cancel₀
Nat.cast_ne_zero
LT.lt.ne'
ENNReal.div_eq_div_iff
ENNReal.ofReal_ne_top
volume_of_add_preimage_eq
closedBall_ae_eq_ball
mul_assoc
Filter.Tendsto.congr'
ENNReal.div_eq_one_iff
tendsto_const_nhds_iff
T5Space.toT1Space
ENNReal.instT5Space
Ergodic
AddMonoid.toNatSMul
Nat.abs_cast
IsStrictOrderedRing.toIsOrderedRing
Int.instIsStrictOrderedRing
Int.instAddLeftMono
Int.instZeroLEOneClass
Int.instCharZero
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ESeminormedAddCommMonoid.toAddCommMonoid
QuotientAddGroup.instTopologicalSpace
Real.pseudoMetricSpace
abs
instLatticeInt
Int.instAddGroup
SubNegMonoid.toZSMul
AddGroup.toSubNegMonoid
MeasureTheory.Measure.measurePreserving_zsmul
QuotientAddGroup.instIsTopologicalAddGroup
compactSpace
abs_pos
lt_trans
zero_lt_one
Nat.one_lt_cast
Int.abs_eq_natAbs
addOrderOf_div_of_gcd_eq_one
pow_pos
LinearOrderedCommMonoidWithZero.toPosMulStrictMono
Nat.instZeroLEOneClass
pos_of_gt
Nat.instCanonicallyOrderedAdd
gcd_one_left
addOrderOf_dvd_iff_zsmul_eq_zero
Int.natCast_natAbs
abs_pow
abs_dvd
dvd_refl
vadd_eq_self_of_preimage_zsmul_eq_self
Filter.EventuallyEq.refl
tendsto_pow_atTop_atTop_of_one_lt
Nat.instIsStrictOrderedRing
StarOrderedRing.toExistsAddOfLE
Nat.instStarOrderedRing
instArchimedeanNat
Filter.eventuallyConst_set'
MeasurableSet.nullMeasurableSet
Filter.atTop_neBot
instIsDirectedOrder
ContinuousAdd.measurableAdd
IsTopologicalAddGroup.toContinuousAdd
MeasureTheory.measurePreserving_add_left
MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant
sub_ne_zero
ne_of_gt
abs_one
DivisibleBy.div_cancel
sub_smul
one_smul
sub_add_cancel
MeasurableEquiv.symm_addLeft
smul_add
zsmul_neg'
neg_smul
neg_add_rev
Mathlib.Tactic.Abel.subst_into_addg
Mathlib.Tactic.Abel.term_atomg
Mathlib.Tactic.Abel.subst_into_negg
Mathlib.Tactic.Abel.term_neg
neg_zero
Mathlib.Tactic.Abel.term_add_constg
zero_add
Mathlib.Tactic.Abel.term_add_termg
Mathlib.Meta.NormNum.IsNat.to_eq
Mathlib.Meta.NormNum.IsInt.to_isNat
Mathlib.Meta.NormNum.isInt_add
Mathlib.Meta.NormNum.isInt_neg
Mathlib.Meta.NormNum.IsNat.to_isInt
add_zero
Mathlib.Tactic.Abel.zero_termg
MeasureTheory.MeasurePreserving.ergodic_conjugate_iff
---
← Back to Index