Documentation Verification Report

Conservative

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

Statistics

Metric	Count
Definitions `Conservative`	1
Theorems `ae_forall_image_mem_imp_frequently_image_mem`, `ae_frequently_mem_of_mem_nhds`, `ae_mem_imp_frequently_image_mem`, `congr_ae`, `exists_gt_measure_inter_ne_zero`, `exists_mem_iterate_mem`, `exists_mem_iterate_mem'`, `frequently_ae_mem_and_frequently_image_mem`, `frequently_measure_inter_ne_zero`, `id`, `inter_frequently_image_mem_ae_eq`, `iterate`, `measureRestrict`, `measure_inter_frequently_image_mem_eq`, `measure_mem_forall_ge_image_notMem_eq_zero`, `of_absolutelyContinuous`, `toQuasiMeasurePreserving`, `conservative`, `conservative_congr`	19
Total	20

MeasureTheory

Definitions

Name	Category	Theorems
`Conservative` 📖	CompData	3 math math: `conservative_congr`, `Conservative.id`, `MeasurePreserving.conservative`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conservative_congr` 📖	mathematical	`ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Conservative`	—	`Measure.instOuterMeasureClass` `Conservative.congr_ae`

MeasureTheory.Conservative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_forall_image_mem_imp_frequently_image_mem` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_all_iff` `instCountableNat` `Filter.Eventually.mono` `ae_mem_imp_frequently_image_mem` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.QuasiMeasurePreserving.iterate` `toQuasiMeasurePreserving` `Filter.map_add_atTop_eq_nat` `Filter.frequently_map` `Filter.Frequently.mono` `add_comm` `Function.iterate_add_apply`
`ae_frequently_mem_of_mem_nhds` 📖	mathematical	`MeasureTheory.Conservative`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ae_mem_imp_frequently_image_mem` `IsOpen.nullMeasurableSet` `TopologicalSpace.isOpen_of_mem_countableBasis` `Filter.Eventually.mono` `MeasureTheory.ae_ball_iff` `TopologicalSpace.countable_countableBasis` `TopologicalSpace.IsTopologicalBasis.mem_nhds_iff` `TopologicalSpace.isBasis_countableBasis` `Filter.Frequently.mono`
`ae_mem_imp_frequently_image_mem` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `forall_swap` `instCountableNat` `Filter.mp_mem` `MeasureTheory.measure_eq_zero_iff_ae_notMem` `measure_mem_forall_ge_image_notMem_eq_zero` `Filter.univ_mem'`
`congr_ae` 📖	—	`MeasureTheory.Conservative` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `of_absolutelyContinuous` `LE.le.absolutelyContinuous_of_ae` `Eq.ge` `MeasureTheory.Measure.QuasiMeasurePreserving.mono` `Eq.le` `toQuasiMeasurePreserving`
`exists_gt_measure_inter_ne_zero` 📖	—	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	—	—	`Filter.Frequently.exists` `Filter.Frequently.and_eventually` `frequently_measure_inter_ne_zero` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder`
`exists_mem_iterate_mem` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Set` `Set.instMembership` `Nat.iterate`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq` `exists_mem_iterate_mem'` `MeasureTheory.measure_congr`
`exists_mem_iterate_mem'` 📖	mathematical	`MeasureTheory.Conservative` `MeasurableSet`	`Set` `Set.instMembership` `Nat.iterate`	—	—
`frequently_ae_mem_and_frequently_image_mem` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Filter.Frequently` `Set` `Set.instMembership` `Nat.iterate` `Filter.atTop` `Nat.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.Frequently.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.Frequently.and_eventually` `MeasureTheory.frequently_ae_mem_iff` `ae_mem_imp_frequently_image_mem`
`frequently_measure_inter_ne_zero` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Filter.Frequently` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Set.preimage` `Nat.iterate` `instZeroENNReal` `Filter.atTop` `Nat.instPreorder`	—	`not_le` `not_imp_comm` `Set.mem_setOf` `Set.exists_max_image` `Set.not_infinite` `Nat.frequently_atTop_iff_infinite` `Set.inter_self` `MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.QuasiMeasurePreserving.iterate` `toQuasiMeasurePreserving` `MeasureTheory.measure_diff_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.measure_biUnion_null_iff` `Set.to_countable` `SetCoe.countable` `instCountableNat` `MeasureTheory.NullMeasurableSet.diff` `MeasureTheory.NullMeasurableSet.biUnion` `exists_mem_iterate_mem` `Set.mem_iUnion₂` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Function.iterate_add`
`id` 📖	mathematical	—	`MeasureTheory.Conservative`	—	`MeasureTheory.Measure.QuasiMeasurePreserving.id` `Function.iterate_id` `Nat.instNontrivial` `MeasureTheory.nonempty_of_measure_ne_zero`
`inter_frequently_image_mem_ae_eq` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set` `Set.instInter` `setOf` `Filter.Frequently` `Set.instMembership` `Nat.iterate` `Filter.atTop` `Nat.instPreorder`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.inter_eventuallyEq_left` `ae_mem_imp_frequently_image_mem`
`iterate` 📖	mathematical	`MeasureTheory.Conservative`	`Nat.iterate`	—	`id` `MeasureTheory.Measure.QuasiMeasurePreserving.iterate` `toQuasiMeasurePreserving` `Filter.Frequently.exists` `MeasureTheory.Measure.instOuterMeasureClass` `frequently_ae_mem_and_frequently_image_mem` `MeasurableSet.nullMeasurableSet` `Nat.exists_lt_modEq_of_infinite` `Nat.frequently_atTop_iff_infinite` `Nat.modEq_iff_dvd'` `LT.lt.le` `LE.le.not_gt` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MulZeroClass.mul_zero` `Function.iterate_mul` `Function.iterate_add_apply` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`measureRestrict` 📖	mathematical	`MeasureTheory.Conservative` `Set.MapsTo`	`MeasureTheory.Measure.restrict`	—	`of_absolutelyContinuous` `MeasureTheory.Measure.absolutelyContinuous_of_le` `MeasureTheory.Measure.restrict_le_self` `MeasureTheory.Measure.QuasiMeasurePreserving.restrict` `toQuasiMeasurePreserving`
`measure_inter_frequently_image_mem_eq` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter` `setOf` `Filter.Frequently` `Set.instMembership` `Nat.iterate` `Filter.atTop` `Nat.instPreorder`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `inter_frequently_image_mem_ae_eq`
`measure_mem_forall_ge_image_notMem_eq_zero` 📖	mathematical	`MeasureTheory.Conservative` `MeasureTheory.NullMeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `setOf` `Set.instMembership` `instZeroENNReal`	—	`Set.setOf_forall` `Set.iInter_congr_Prop` `MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.biInter` `Set.to_countable` `SetCoe.countable` `instCountableNat` `MeasureTheory.NullMeasurableSet.compl` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.QuasiMeasurePreserving.iterate` `toQuasiMeasurePreserving` `exists_gt_measure_inter_ne_zero` `MeasureTheory.nonempty_of_measure_ne_zero` `LT.lt.le` `GT.gt.lt`
`of_absolutelyContinuous` 📖	—	`MeasureTheory.Conservative` `MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Measure.QuasiMeasurePreserving`	—	—	`exists_mem_iterate_mem'`
`toQuasiMeasurePreserving` 📖	mathematical	`MeasureTheory.Conservative`	`MeasureTheory.Measure.QuasiMeasurePreserving`	—	—

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conservative` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.Conservative`	—	`quasiMeasurePreserving` `exists_mem_iterate_mem` `MeasurableSet.nullMeasurableSet`

---

← Back to Index