mathlib

d6fad0e5 - feat(analysis/bounded_variation): define `variation_on_from_to` (#18040)

feat(analysis/bounded_variation): define `variation_on_from_to` (#18040) … and refactor `has_locally_bounded_variation_on.exists_monotone_on_sub_monotone_on` using it. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>