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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 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