mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable

Open sgouezel opened this issue 3 years ago • 3 comments

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.

I will split this into many smaller PRs, but I open this PR to show the endgoal.

  • [x] depends on: #16549
  • [x] depends on: #16682
  • [x] depends on: #16683
  • [x] depends on: #16684

Open in Gitpod

sgouezel avatar Sep 28 '22 08:09 sgouezel

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16549~~
  • ~~leanprover-community/mathlib#16682~~
  • ~~leanprover-community/mathlib#16683~~
  • ~~leanprover-community/mathlib#16684~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 12 '22 20:10 mathlib-dependent-issues-bot

LGTM, other than the build errors

bors d+

fpvandoorn avatar Oct 13 '22 10:10 fpvandoorn

:v: sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Oct 13 '22 10:10 bors[bot]

bors r+

sgouezel avatar Oct 14 '22 06:10 sgouezel

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 14 '22 10:10 bors[bot]