New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Rademacher theorem #7003
Conversation
First calculus prerequisites for Rademacher theorem in #7003. Add a few lemmas that were available for `FDeriv` but not for `Deriv`, weaken assumptions here and there.
Prerequisite for Rademacher's theorem in #7003 We currently have in mathlib the Fréchet derivative, and the derivative of maps defined on the scalar field. In this PR, we introduce another notion, the derivative along a line. It is more elementary (but less well behaved) than the full Fréchet derivative. The API is essentially copied from the file on the one-dimensional derivative, with a few additions that have proved useful for Rademacher's theorem. The API could definitely be expanded, but it's already heavy... I have put everything in the single file `LineDeriv/Basic.lean`, mimicking the directory structure for `FDeriv` and `Deriv` and leaving open the possibility to add other files in this folder with more API.
Last prerequisite for Rademacher theorem in #7003. Along the way, we weaken the second-countability assumptions for strong measurability of the derivative and the right derivative.
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Thanks! |
We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.
Build failed: |
bors retry |
We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.
This PR was included in a batch that was canceled, it will be automatically retried |
We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.