Commit 2023-05-21 17:05 9b4547ad

View on Github →

feat: port MeasureTheory.Measure.Stieltjes (#4067)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Stieltjes.lean

added theorem MeasureTheory.tendsto_measure_Ici_atBot

added theorem MeasureTheory.tendsto_measure_Ico_atTop

added theorem MeasureTheory.tendsto_measure_Iic_atTop

added theorem MeasureTheory.tendsto_measure_Ioc_atBot

added theorem Monotone.stieltjesFunction_eq

added theorem StieltjesFunction.borel_le_measurable

added theorem StieltjesFunction.countable_leftLim_ne

added theorem StieltjesFunction.iInf_Ioi_eq

added theorem StieltjesFunction.iInf_rat_gt_eq

added theorem StieltjesFunction.id_leftLim

added def StieltjesFunction.length

added theorem StieltjesFunction.length_Ioc

added theorem StieltjesFunction.length_empty

added theorem StieltjesFunction.length_mono

added theorem StieltjesFunction.length_subadditive_Icc_Ioo

added theorem StieltjesFunction.measurableSet_Ioi

added theorem StieltjesFunction.measure_Icc

added theorem StieltjesFunction.measure_Ici

added theorem StieltjesFunction.measure_Ico

added theorem StieltjesFunction.measure_Iic

added theorem StieltjesFunction.measure_Ioc

added theorem StieltjesFunction.measure_Ioo

added theorem StieltjesFunction.measure_singleton

added theorem StieltjesFunction.measure_univ

added theorem StieltjesFunction.mono

added theorem StieltjesFunction.outer_Ioc

added theorem StieltjesFunction.outer_le_length

added theorem StieltjesFunction.outer_trim

added theorem StieltjesFunction.rightLim_eq

added theorem StieltjesFunction.right_continuous

added structure StieltjesFunction

added theorem exists_seq_antitone_tendsto_atTop_atBot

added theorem exists_seq_monotone_tendsto_atTop_atTop

added theorem iInf_Ioi_eq_iInf_rat_gt

added theorem iSup_eq_iSup_subseq_of_antitone

added theorem rightLim_eq_of_tendsto

added theorem rightLim_eq_sInf