RadonNikodym

📁 Source: Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean

Statistics

Metric	Count
Definitions	0
Theorems absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, withDensityᵥ_rnDeriv_eq, withDensityᵥ_rnDeriv_smul	3
Total	3

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensityᵥ_rnDeriv_smul 📖	mathematical	Measure.AbsolutelyContinuous Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Measure.withDensityᵥ Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField ENNReal.toReal Measure.rnDeriv	—	withDensityᵥ_smul_eq_withDensityᵥ_withDensity' Measurable.aemeasurable Measure.measurable_rnDeriv Measure.rnDeriv_lt_top integrable_rnDeriv_smul_iff Measure.withDensity_rnDeriv_eq

MeasureTheory.SignedMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.Measure.withDensityᵥ Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal rnDeriv	—	withDensityᵥ_rnDeriv_eq MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous
withDensityᵥ_rnDeriv_eq 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure	MeasureTheory.Measure.withDensityᵥ Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal rnDeriv	—	MeasureTheory.VectorMeasure.ext MeasureTheory.withDensityᵥ_apply integrable_rnDeriv rnDeriv_def MeasureTheory.integral_sub MeasureTheory.Integrable.integrableOn Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top LT.lt.ne MeasureTheory.Measure.lintegral_rnDeriv_lt_top MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.Measure.setIntegral_toReal_rnDeriv MeasureTheory.IsFiniteMeasure.toSigmaFinite totalVariation_absolutelyContinuous_iff Equiv.right_inv absolutelyContinuous_ennreal_iff toSignedMeasure_toJordanDecomposition instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.sub_apply MeasureTheory.Measure.toSignedMeasure_apply_measurable MeasureTheory.measureReal_def

---

← Back to Index