Commit 2026-02-23 19:12 5730ae8f

View on Github →

feat: bounded variation functions have left and right limits, and limits at infinity (#34559) Needed for #34055.

Estimated changes

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

added theorem BoundedVariationOn.continuousWithinAt_leftLim

added theorem BoundedVariationOn.continuousWithinAt_rightLim

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici

added theorem BoundedVariationOn.exists_tendsto_atBot

added theorem BoundedVariationOn.exists_tendsto_atTop

added theorem BoundedVariationOn.exists_tendsto_left

added theorem BoundedVariationOn.exists_tendsto_left_of_filter

added theorem BoundedVariationOn.exists_tendsto_right

added theorem BoundedVariationOn.leftLim

added theorem BoundedVariationOn.ofDual

added theorem BoundedVariationOn.rightLim

added theorem BoundedVariationOn.tendsto_atBot_limUnder

added theorem BoundedVariationOn.tendsto_atTop_limUnder

added theorem BoundedVariationOn.tendsto_eVariationOn_Icc_zero_left

added theorem BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right

added theorem BoundedVariationOn.tendsto_eVariationOn_Ici_zero

added theorem BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter

added theorem BoundedVariationOn.tendsto_eVariationOn_Ico_zero

added theorem BoundedVariationOn.tendsto_eVariationOn_Iic_zero

added theorem BoundedVariationOn.tendsto_eVariationOn_Ioc_zero

added theorem BoundedVariationOn.tendsto_leftLim

added theorem BoundedVariationOn.tendsto_rightLim

added theorem eVariationOn.boundedVariation_ofDual

modified theorem eVariationOn.comp_ofDual

added theorem eVariationOn.congr

added theorem eVariationOn.eVariationOn_eq_strictMonoOn

added theorem eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt

added theorem eVariationOn.eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt

added theorem eVariationOn.eVariationOn_leftLim_le

added theorem eVariationOn.eVariationOn_rightLim_le

added theorem eVariationOn.exists_lt_eVariationOn_inter_Icc

modified theorem eVariationOn.sum_le

modified theorem eVariationOn.sum_le_of_monotoneOn_Icc

modified theorem eVariationOn.sum_le_of_monotoneOn_Iic

added theorem variationOnFromTo.abs_le_eVariationOn