RadonNikodym

📁 Source: Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean

Statistics

Metric	Count
Definitions	0
Theorems rnDeriv_map, rnDeriv_map_ae_eq_trim, rnDeriv_trim, toReal_rnDeriv_map, toReal_rnDeriv_map_ae_eq_trim, toReal_rnDeriv_trim	6
Total	6

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rnDeriv_map 📖	mathematical	Measure.AbsolutelyContinuous Measurable	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.rnDeriv Measure.map condLExp MeasurableSpace.comap	—	SigmaFinite.of_map Measurable.aemeasurable Measure.instOuterMeasureClass ae_of_ae_map Measure.rnDeriv_ne_top IsFiniteMeasure.toSigmaFinite Measure.isFiniteMeasure_map condLExp_ne_top Measure.lintegral_rnDeriv Measure.haveLebesgueDecomposition_of_sigmaFinite instSFiniteOfSigmaFinite Real.instCompleteSpace toReal_condLExp Measure.measurable_rnDeriv Filter.mp_mem toReal_rnDeriv_map Filter.univ_mem' ENNReal.toReal_eq_toReal_iff'
rnDeriv_map_ae_eq_trim 📖	mathematical	Measure.AbsolutelyContinuous Measurable	Filter.EventuallyEq ENNReal ae Measure MeasurableSpace.comap Measure.instFunLike Measure.instOuterMeasureClass Measure.trim Measurable.comap_le Measure.rnDeriv Measure.map condLExp	—	Measure.instOuterMeasureClass Measurable.comap_le StronglyMeasurable.ae_eq_trim_iff ENNReal.instMetrizableSpace Measurable.stronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable ENNReal.borelSpace MeasurableSet.preimage Measure.measurable_rnDeriv measurable_condLExp rnDeriv_map
rnDeriv_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measure.AbsolutelyContinuous	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim Measure.rnDeriv ENNReal.ofReal condExp Real Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal.toReal	—	Filter.mp_mem Measure.instOuterMeasureClass Real.instCompleteSpace Measure.rnDeriv_ne_top IsFiniteMeasure.toSigmaFinite isFiniteMeasure_trim toReal_rnDeriv_trim Filter.univ_mem' ENNReal.ofReal_toReal
toReal_rnDeriv_map 📖	mathematical	Measure.AbsolutelyContinuous Measurable	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal.toReal Measure.rnDeriv Measure.map condExp MeasurableSpace.comap Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Measurable.comap_le SigmaFinite.of_map Measurable.aemeasurable measurable_iff_comap_le le_rfl map_trim_comap ae_eq_condExp_of_forall_setIntegral_eq Real.instCompleteSpace Measure.integrable_toReal_rnDeriv Integrable.integrableOn integrable_map_measure Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal Measure.measurable_rnDeriv Measure.isFiniteMeasure_map setIntegral_map Measure.setIntegral_toReal_rnDeriv IsFiniteMeasure.toSigmaFinite Measure.AbsolutelyContinuous.map measureReal_def Measure.map_apply
toReal_rnDeriv_map_ae_eq_trim 📖	mathematical	Measure.AbsolutelyContinuous Measurable	Filter.EventuallyEq Real ae Measure MeasurableSpace.comap Measure.instFunLike Measure.instOuterMeasureClass Measure.trim Measurable.comap_le ENNReal.toReal Measure.rnDeriv Measure.map condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Measure.instOuterMeasureClass Measurable.comap_le Real.instCompleteSpace StronglyMeasurable.ae_eq_trim_iff EMetricSpace.metrizableSpace Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace MeasurableSet.preimage Measurable.ennreal_toReal Measure.measurable_rnDeriv Set.preimage_comp stronglyMeasurable_condExp toReal_rnDeriv_map
toReal_rnDeriv_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim ENNReal.toReal Measure.rnDeriv condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Measure.instOuterMeasureClass Real.instCompleteSpace ae.congr_simp trim_eq_map Measurable.comap_le measurable_id'' toReal_rnDeriv_map_ae_eq_trim MeasurableSpace.comap_id

---

← Back to Index