with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)

Commit

4 years ago

feat(measure_theory/measure/with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)

Author

kex-y

Parents

232ff445

mathlib 8a1fc68e - feat(measure_theory/measure/with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)

mathlib
8a1fc68e - feat(measure_theory/measure/with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)