Extreme

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

Statistics

Metric	Count
Definitions	0
Theorems eq_of_absolutelyContinuous, eq_of_absolutelyContinuous_measure_univ_eq, eq_smul_of_absolutelyContinuous, iff_mem_extremePoints, iff_mem_extremePoints_measure_univ_eq, mem_extremePoints, mem_extremePoints_measure_univ_eq, of_mem_extremePoints, of_mem_extremePoints_measure_univ_eq	9
Total	9

Ergodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_absolutelyContinuous 📖	—	Ergodic MeasureTheory.MeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	—	—	eq_of_absolutelyContinuous_measure_univ_eq MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.IsProbabilityMeasure.measure_univ
eq_of_absolutelyContinuous_measure_univ_eq 📖	—	Ergodic MeasureTheory.MeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	—	IsScalarTower.right eq_smul_of_absolutelyContinuous eq_or_ne smul_zero one_smul
eq_smul_of_absolutelyContinuous 📖	mathematical	Ergodic MeasureTheory.MeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq toMeasurePreserving IsScalarTower.right ae_eq_const_of_ae_eq_comp₀ MeasurableSpace.countablySeparated_of_separatesPoints BorelSpace.countablyGenerated ENNReal.borelSpace ENNReal.instSecondCountableTopology separatesPointsOfOpensMeasurableSpaceOfT0Space BorelSpace.opensMeasurable T6Space.toT0Space instT6SpaceOfMetrizableSpace ENNReal.instMetrizableSpace Measurable.nullMeasurable MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.Measure.ext MeasureTheory.Measure.setLIntegral_rnDeriv MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.lintegral_congr_ae Filter.EventuallyEq.filter_mono MeasureTheory.ae_mono MeasureTheory.Measure.restrict_le_self MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter
iff_mem_extremePoints 📖	mathematical	—	Ergodic MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving MeasureTheory.IsProbabilityMeasure	—	IsScalarTower.right mem_extremePoints of_mem_extremePoints
iff_mem_extremePoints_measure_univ_eq 📖	mathematical	—	Ergodic MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving DFunLike.coe MeasureTheory.Measure.instFunLike Set.univ	—	IsScalarTower.right mem_extremePoints_measure_univ_eq of_mem_extremePoints_measure_univ_eq MeasureTheory.measure_ne_top
mem_extremePoints 📖	mathematical	Ergodic	MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving MeasureTheory.IsProbabilityMeasure	—	IsScalarTower.right MeasureTheory.IsProbabilityMeasure.measure_univ mem_extremePoints_measure_univ_eq MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure
mem_extremePoints_measure_univ_eq 📖	mathematical	Ergodic	MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving DFunLike.coe MeasureTheory.Measure.instFunLike Set.univ	—	IsScalarTower.right mem_extremePoints_iff_left toMeasurePreserving MeasureTheory.measure_lt_top eq_of_absolutelyContinuous_measure_univ_eq MeasureTheory.Measure.AbsolutelyContinuous.add_right MeasureTheory.Measure.absolutelyContinuous_smul LT.lt.ne'
of_mem_extremePoints 📖	mathematical	MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving MeasureTheory.IsProbabilityMeasure	Ergodic	—	IsScalarTower.right of_mem_extremePoints_measure_univ_eq ENNReal.one_ne_top
of_mem_extremePoints_measure_univ_eq 📖	mathematical	MeasureTheory.Measure Set Set.instMembership Set.extremePoints ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder MeasureTheory.Measure.instAddCommMonoid MeasureTheory.Measure.instSMul Algebra.toSMul Algebra.id IsScalarTower.right setOf MeasureTheory.MeasurePreserving DFunLike.coe MeasureTheory.Measure.instFunLike Set.univ	Ergodic	—	IsScalarTower.right eq_or_ne MeasureTheory.Measure.measure_univ_eq_zero zero_measure MeasureTheory.MeasurePreserving.measurable lt_top_iff_ne_top MeasureTheory.MeasurePreserving.smul_measure MeasureTheory.MeasurePreserving.restrict_preimage MeasureTheory.Measure.smul_apply MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.cond_isProbabilityMeasure smul_eq_mul mul_one MeasureTheory.Measure.instOuterMeasureClass MeasurableSet.compl Set.preimage_compl ENNReal.div_pos ENNReal.add_div MeasureTheory.measure_add_measure_compl ENNReal.div_self smul_smul ENNReal.div_mul_cancel ENNReal.mul_inv_cancel one_smul MeasureTheory.Measure.restrict_add_restrict_compl ProbabilityTheory.cond_apply Set.inter_compl_self MeasureTheory.measure_empty MulZeroClass.mul_zero

---

← Back to Index