mathlib

aadde303 - 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.