2021-10-01 20:35
src/measure_theory/measure/with_density_vector_measure.lean
feat(measure_theory/function/conditional_expectation): conditional expectation on real functions equal Radon-Nikodym derivative (#9378)
Added measure_theory.integrable.with_densityᵥ_trim_eq_integral