Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 23:18 432da5f8

View on Github →

feat(measure_theory/integration): add lintegral_with_density_eq_lintegral_mul (#4350) This is Exercise 1.2.1 from Terence Tao's "An Epsilon of Room"

Estimated changes

Modified docs/references.bib

Modified src/measure_theory/integration.lean

modified theorem measure_theory.lintegral_add

modified theorem measure_theory.lintegral_add_measure

modified theorem measure_theory.lintegral_const_mul

modified theorem measure_theory.lintegral_smul_measure

modified theorem measure_theory.lintegral_sum_measure

added theorem measure_theory.lintegral_with_density_eq_lintegral_mul

modified theorem measure_theory.with_density_apply