RadonNikodym

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

Statistics

Metric	Count
Definitions	0
Theorems rnDeriv_comp_aeEq, singularPart, withDensity_rnDeriv	3
Total	3

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rnDeriv_comp_aeEq 📖	mathematical	MeasureTheory.MeasurePreserving	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.of_forall_eventually_lt_iff ENNReal.instOrderTopology ENNReal.instSecondCountableTopology MeasureTheory.instCountableInterFilter MeasureTheory.Measure.measurable_rnDeriv measurableSet_Iio BorelSpace.opensMeasurable ENNReal.borelSpace instClosedIciTopology OrderTopology.to_orderClosedTopology MeasureTheory.measure_diff_symm MeasurableSet.nullMeasurableSet measurable measure_preimage MeasureTheory.measure_ne_top Mathlib.Tactic.Contrapose.contrapose₁ ne_of_gt MeasureTheory.Measure.setLIntegral_rnDeriv MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.setLIntegral_strict_mono MeasurableSet.diff measurable_const Filter.Eventually.of_forall MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter MeasureTheory.setLIntegral_mono not_lt Filter.EventuallyLE.antisymm MeasureTheory.ae_le_set Filter.EventuallyEq.mem_iff Filter.EventuallyEq.trans MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp quasiMeasurePreserving Filter.EventuallyEq.symm MeasureTheory.Measure.rnDeriv_withDensity MeasureTheory.Measure.withDensity.instIsFiniteMeasure withDensity_rnDeriv MeasureTheory.withDensity_absolutelyContinuous
singularPart 📖	mathematical	MeasureTheory.MeasurePreserving	MeasureTheory.Measure.singularPart	—	MeasureTheory.Measure.MutuallySingular.symm MeasureTheory.Measure.mutuallySingular_singularPart MeasureTheory.Measure.singularPart_eq_restrict MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.mem_ae_iff Filter.eventuallyEq_univ MeasureTheory.ae_eq_univ_iff_measure_eq MeasureTheory.Measure.singularPart.instIsFiniteMeasure MeasurableSet.nullMeasurableSet measurable MeasureTheory.Measure.add_apply MeasureTheory.withDensity_absolutelyContinuous measure_preimage zero_add MeasureTheory.Measure.rnDeriv_add_singularPart MeasureTheory.measure_add_measure_compl add_zero preimage_null restrict_preimage
withDensity_rnDeriv 📖	mathematical	MeasureTheory.MeasurePreserving	MeasureTheory.Measure.withDensity MeasureTheory.Measure.rnDeriv	—	measurable MeasureTheory.Measure.ext MeasureTheory.measure_ne_top MeasureTheory.Measure.singularPart.instIsFiniteMeasure MeasureTheory.Measure.map_apply MeasureTheory.Measure.add_apply MeasureTheory.Measure.rnDeriv_add_singularPart MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite measure_preimage singularPart MeasurableSet.nullMeasurableSet

---

← Back to Index