Commit 2026-01-29 16:43 f8f80fe4

View on Github →

feat: improve Stieltjes measure file (#34415) Notably, remove assumptions that the order has no max or no min in several lemmas. Cherry picked from #34055.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

modified theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot

modified theorem StieltjesFunction.isFiniteMeasure

added theorem StieltjesFunction.isFiniteMeasure_of_forall_abs_le

modified theorem StieltjesFunction.isProbabilityMeasure

modified theorem StieltjesFunction.measure_Ici

modified theorem StieltjesFunction.measure_Iic

modified theorem StieltjesFunction.measure_Iio

modified theorem StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot

modified theorem StieltjesFunction.measure_Ioi

added theorem StieltjesFunction.measure_botSet

modified theorem StieltjesFunction.measure_univ

modified theorem StieltjesFunction.measure_univ_of_tendsto_atBot_atBot

added theorem botSet_eq_singleton_of_isBot