mathlib

71429ce7 - feat(analysis/bounded_variation): functions of bounded variation are ae differentiable (#16680)

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable (#16680) We define functions of bounded variation. We show that such functions are a difference of monotone functions, and deduce that they are differentiable almost everywhere. This applies in particular to Lipschitz functions.