mathlib3

3eea1091 - feat(measure_theory/interval_integral): introduce `∫ x in a..b, f x`, prove FTC-1 (#3640)

feat(measure_theory/interval_integral): introduce `∫ x in a..b, f x`, prove FTC-1 (#3640) Define `∫ x in a..b, f x ∂μ` as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. With this definition for a probability measure `μ` we have `F_μ(b)-F_μ(a)=∫ x in a..b, f x ∂μ`, where `F_μ` is the cumulative distribution function.