WithDensity

📁 Source: Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean

Statistics

Metric	Count
Definitions withDensityᵥ	1
Theorems ae_eq_of_withDensityᵥ_eq, withDensityᵥ_eq_iff, withDensityᵥ_trim_absolutelyContinuous, withDensityᵥ_trim_eq_integral, withDensityᵥ_absolutelyContinuous, congr_ae, withDensityᵥ_add, withDensityᵥ_add', withDensityᵥ_apply, withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, withDensityᵥ_neg, withDensityᵥ_neg', withDensityᵥ_smul, withDensityᵥ_smul', withDensityᵥ_smul_eq_withDensityᵥ_withDensity, withDensityᵥ_smul_eq_withDensityᵥ_withDensity', withDensityᵥ_sub, withDensityᵥ_sub', withDensityᵥ_toReal, withDensityᵥ_zero	20
Total	21

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensityᵥ_add 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Measure.withDensityᵥ Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure VectorMeasure.instAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	VectorMeasure.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup withDensityᵥ_apply Integrable.add VectorMeasure.add_apply integral_add Integrable.integrableOn
withDensityᵥ_add' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Measure.withDensityᵥ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure VectorMeasure.instAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	withDensityᵥ_add
withDensityᵥ_apply 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasurableSet	VectorMeasure.measureOf' ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Measure.withDensityᵥ integral Measure.restrict	—	Measure.withDensityᵥ.eq_1
withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Measure.withDensityᵥ Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SignedMeasure VectorMeasure.instSub Real.instAddCommGroup instIsTopologicalAddGroupReal Measure.toSignedMeasure Measure.withDensity ENNReal.ofReal isFiniteMeasure_withDensity_ofReal AEStronglyMeasurable HasFiniteIntegral ContinuousENorm.toENorm Real.instNeg SeminormedAddCommGroup.toPseudoMetricSpace Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Integrable.neg	—	VectorMeasure.ext instIsTopologicalAddGroupReal isFiniteMeasure_withDensity_ofReal Integrable.neg withDensityᵥ_apply integral_eq_lintegral_pos_part_sub_lintegral_neg_part Integrable.integrableOn VectorMeasure.sub_apply Measure.toSignedMeasure_apply_measurable measureReal_def withDensity_apply
withDensityᵥ_neg 📖	mathematical	—	Measure.withDensityᵥ Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure.instNeg SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup VectorMeasure.ext VectorMeasure.neg_apply withDensityᵥ_apply integral_neg Integrable.neg Measure.withDensityᵥ.eq_1 integrable_neg_iff neg_zero
withDensityᵥ_neg' 📖	mathematical	—	Measure.withDensityᵥ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure.instNeg SeminormedAddCommGroup.toIsTopologicalAddGroup	—	withDensityᵥ_neg
withDensityᵥ_smul 📖	mathematical	—	Measure.withDensityᵥ Function.hasSMul 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule VectorMeasure VectorMeasure.instSMul UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul VectorMeasure.ext withDensityᵥ_apply Integrable.smul VectorMeasure.smul_apply integral_smul NormedSpace.toNormSMulClass zero_smul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup withDensityᵥ_zero Measure.withDensityᵥ.eq_1 integrable_smul_iff smul_zero
withDensityᵥ_smul' 📖	mathematical	—	Measure.withDensityᵥ 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule VectorMeasure VectorMeasure.instSMul UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul	—	withDensityᵥ_smul
withDensityᵥ_smul_eq_withDensityᵥ_withDensity 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Pi.smul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	Measure.withDensityᵥ Measure.withDensity ENNReal.ofNNReal	—	VectorMeasure.ext withDensityᵥ_apply integrable_withDensity_iff_integrable_smul₀ setIntegral_withDensity_eq_setIntegral_smul₀ AEMeasurable.restrict
withDensityᵥ_smul_eq_withDensityᵥ_withDensity' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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.withDensityᵥ Measure.withDensity	—	Measure.instOuterMeasureClass withDensity_congr_ae coe_toNNReal_ae_eq withDensityᵥ_smul_eq_withDensityᵥ_withDensity AEMeasurable.ennreal_toNNReal
withDensityᵥ_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Measure.withDensityᵥ Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure.instSub NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup sub_eq_add_neg IsTopologicalAddGroup.toContinuousAdd withDensityᵥ_add Integrable.neg withDensityᵥ_neg
withDensityᵥ_sub' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Measure.withDensityᵥ SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure.instSub NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	withDensityᵥ_sub
withDensityᵥ_toReal 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.withDensityᵥ Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal.toReal Measure.toSignedMeasure Measure.withDensity isFiniteMeasure_withDensity	—	integrable_toReal_of_lintegral_ne_top VectorMeasure.ext isFiniteMeasure_withDensity withDensityᵥ_apply Measure.toSignedMeasure_apply_measurable measureReal_def withDensity_apply integral_toReal AEMeasurable.restrict ae_lt_top' ne_top_of_le_ne_top setLIntegral_univ lintegral_mono_set Set.subset_univ
withDensityᵥ_zero 📖	mathematical	—	Measure.withDensityᵥ Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VectorMeasure.instZero	—	VectorMeasure.ext Pi.zero_def withDensityᵥ_apply integrable_zero integral_zero

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_withDensityᵥ_eq 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.Measure.withDensityᵥ	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_of_forall_setIntegral_eq MeasureTheory.withDensityᵥ_apply
withDensityᵥ_eq_iff 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.Measure.withDensityᵥ Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq_of_withDensityᵥ_eq MeasureTheory.WithDensityᵥEq.congr_ae
withDensityᵥ_trim_absolutelyContinuous 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.VectorMeasure.AbsolutelyContinuous ENNReal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.VectorMeasure.trim MeasureTheory.Measure.withDensityᵥ MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.Measure.trim	—	MeasureTheory.VectorMeasure.trim_measurableSet_eq MeasureTheory.withDensityᵥ_apply MeasureTheory.Measure.restrict_eq_zero MeasureTheory.trim_measurableSet_eq MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable MeasureTheory.integral_zero_measure
withDensityᵥ_trim_eq_integral 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasurableSet	MeasureTheory.VectorMeasure.measureOf' ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.trim MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.integral MeasureTheory.Measure.restrict	—	MeasureTheory.VectorMeasure.trim_measurableSet_eq MeasureTheory.withDensityᵥ_apply

MeasureTheory.Measure

Definitions

Name	Category	Theorems
withDensityᵥ 📖	CompOp	25 math math: MeasureTheory.withDensityᵥ_sub, MeasureTheory.Integrable.withDensityᵥ_eq_iff, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, MeasureTheory.withDensityᵥ_add', MeasureTheory.withDensityᵥ_neg', MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, withDensityᵥ_absolutelyContinuous, MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity', MeasureTheory.withDensityᵥ_neg, MeasureTheory.rnDeriv_ae_eq_condExp, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, MeasureTheory.withDensityᵥ_apply, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, MeasureTheory.withDensityᵥ_add, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.withDensityᵥ_toReal, MeasureTheory.WithDensityᵥEq.congr_ae, MeasureTheory.withDensityᵥ_zero, MeasureTheory.withDensityᵥ_sub', MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity, MeasureTheory.withDensityᵥ_smul, MeasureTheory.withDensityᵥ_rnDeriv_smul, MeasureTheory.withDensityᵥ_smul'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensityᵥ_absolutelyContinuous 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous Real ENNReal ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal toENNRealVectorMeasure	—	MeasureTheory.withDensityᵥ_apply restrict_zero_set toENNRealVectorMeasure_apply_measurable MeasureTheory.integral_zero_measure withDensityᵥ.eq_1 MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero

MeasureTheory.WithDensityᵥEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_ae 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.withDensityᵥ	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.VectorMeasure.ext MeasureTheory.withDensityᵥ_apply MeasureTheory.Integrable.congr MeasureTheory.integral_congr_ae MeasureTheory.ae_restrict_of_ae Filter.EventuallyEq.symm MeasureTheory.Measure.withDensityᵥ.eq_1

---

← Back to Index