Commit 2024-12-06 15:40 574c5f1b

View on Github →

feat(MeasureTheory): Stieltjes measure of various intervals (#19625) From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

added theorem StieltjesFunction.measure_Ici_of_tendsto_atTop_atTop

added theorem StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot

added theorem StieltjesFunction.measure_Iio

added theorem StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot

added theorem StieltjesFunction.measure_Ioi

added theorem StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop

added theorem StieltjesFunction.measure_univ_of_tendsto_atBot_atBot

added theorem StieltjesFunction.measure_univ_of_tendsto_atTop_atTop

added theorem StieltjesFunction.measure_zero

added theorem StieltjesFunction.zero_apply