mathlib3

3689655d - feat(measure_theory/stieltjes_measure): Stieltjes measures associated to monotone functions (#8266)

feat(measure_theory/stieltjes_measure): Stieltjes measures associated to monotone functions (#8266) Given a monotone right-continuous real function `f`, there exists a measure giving mass `f b - f a` to the interval `(a, b]`. These measures are called Stieltjes measures, and are especially important in probability theory. The real Lebesgue measure is a particular case of this construction, for `f x = x`. This PR extends the already existing construction of the Lebesgue measure to cover all Stieltjes measures.