2021-09-16 11:34
src/measure_theory/function/l1_space.lean
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)
Added measure_theory.is_finite_measure_with_density_of_real