Commit 2026-06-08 11:39 a8b97f6e
View on Github →feat: a bounded variation function is the difference of two monotone functions that add up to the variation (#40289) We already have this lemma, but without the information that the monotone functions add up to the variation. And the construction needs to be a little bit more clever to get this.