feat(analysis/calculus): bounded variation functions (#16683)
feat(analysis/calculus): bounded variation functions (#16683)

We define bounded variation functions, and prove that such a function is the difference of two monotone functions. We also show that Lipschitz functions have bounded variation.





leanprover-community/mathlib,leanprover-community/mathlib