Commit 2021-08-12 17:46 3689655d
View on Github →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.