Skip to content
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

Lebesgue differentiation for continuous functions #972

Merged
merged 13 commits into from
Aug 22, 2023

Conversation

zstone1
Copy link
Contributor

@zstone1 zstone1 commented Jul 9, 2023

More work towards fundamental theorem of calculus, this is the "easy" part of the last track in #965. Most of the proof is shuffling around absolute values signs and standard error bounds. The only interesting detail is that we really do need f to be integrable in a neighborhood around x otherwise it's not clear what the limit actually means.

I prove a couple lemmas that could maybe go in a more helpful location. If you have recommendations, I'm happy to oblige.

Motivation for this change
Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • [] added corresponding documentation in the headers
Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@zstone1 zstone1 added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jul 9, 2023
@zstone1 zstone1 marked this pull request as ready for review July 10, 2023 21:26
@affeldt-aist affeldt-aist self-requested a review July 27, 2023 13:33
@affeldt-aist affeldt-aist added this to the 0.6.5 milestone Aug 5, 2023
@affeldt-aist affeldt-aist mentioned this pull request Aug 8, 2023
2 tasks
zstone1 and others added 8 commits August 8, 2023 17:58
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I proposed a few minor improvements in the last commit.
I would like also to propose to use ball x r instead of ] x - r, x +r[ otherwise it looks like
we are not using an already available identifier that could make it clearer to put together
lemmas about centered, open intervals (that are also important in Vitali's lemma and theorem which also have lemmas about centered, closed intervals).
Also, what about using "r +* 2" instead of "2 * r"? There are many lemmas about the former in ssrnum.v that could maybe trigger small optimizations in calculation steps.
I do not want to make these blocking requests because arguably these are minor issues but being homogeneous about these presentation issues could help factorizing further results.

@affeldt-aist
Copy link
Member

last commit was just to fix the changelog

@zstone1
Copy link
Contributor Author

zstone1 commented Aug 8, 2023

These suggestions seem very sensible. I'll make an update in the next day or two.

@affeldt-aist
Copy link
Member

The last commit is only minor fixes, I'll mege as soon as the CI is as green as it can be.

@affeldt-aist
Copy link
Member

(I changed the changelog because the new negligible_integral is not exactly a generalization I think. Many lemmas come in two flavors: for non-negative functions and for integrable functions. This lemma is an example. Lemmas about non-negative functions are prefixed with ge0_, which explains the name change.)

@affeldt-aist affeldt-aist merged commit 909e6c1 into math-comp:master Aug 22, 2023
affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Aug 23, 2023
* interval topology facts

* weakening continuity

* minor improvements

- minor gen. of integral_le_bound
- move lemmas to more appropriate locations
- rebase on master to use measurable_compact

* using ball instead of intervals in the statement

* using natmul notation

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Sep 5, 2023
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Sep 7, 2023
* interval topology facts

* weakening continuity

* minor improvements

- minor gen. of integral_le_bound
- move lemmas to more appropriate locations
- rebase on master to use measurable_compact

* using ball instead of intervals in the statement

* using natmul notation

---------

Co-authored-by: Reynald Affeldt <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants