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

generalizations #1147

Merged
merged 3 commits into from
Jan 18, 2024
Merged

Conversation

affeldt-aist
Copy link
Member

Motivation for this change

This generalizes a few technical lemmas in realfun.v

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.

@affeldt-aist affeldt-aist added enhancement ✨ This issue/PR is about adding new features enhancing the library TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. labels Jan 11, 2024
@affeldt-aist affeldt-aist added this to the 0.6.8 milestone Jan 11, 2024
@affeldt-aist
Copy link
Member Author

The proofs are a bit longer but this is a strict generalizations, since the CI is green, I plan to merge soon @CohenCyril @zstone1

@CohenCyril
Copy link
Member

CohenCyril commented Jan 17, 2024

Looks good to me, and we should merge.

That beeing said, the proofs might be shorter by doing a wlog that goes back to the previous statement.
(The wlog should change f with a patch of f with a small enough value after the new bound, not to affect the local behaviour around a^+.)

However, we may have more local lemmas asserting the existence of the limit, e.g.

Lemma nonincreasing_at_right_is_cvg (f : R -> R) a :
    (\forall x \near a^'+, {in `]a, x[, nonincreasing_fun f}) ->
    (\forall x \near a^'+, has_ubound (f @` ]a, x[) ->
  cvg (f x @[x --> a ^'+]).

but it can wait for another PR

@zstone1
Copy link
Contributor

zstone1 commented Jan 17, 2024

Agreed I'm happy to merge anything that makes the code better.

On a topological note, the "right-sided topology on R" AKA the "Sogenfrey line" captures a lot of this nicely. So you can talk about "locally in the Sogenfrey line". This has come up before, so maybe I'll write a PR to add it with the relevant lemmas for this application.

@affeldt-aist affeldt-aist merged commit cb07aa9 into math-comp:master Jan 18, 2024
27 of 28 checks passed
affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Jan 19, 2024
@affeldt-aist affeldt-aist mentioned this pull request Jan 19, 2024
proux01 pushed a commit to affeldt-aist/analysis that referenced this pull request Jan 20, 2024
proux01 pushed a commit that referenced this pull request Jan 20, 2024
* generalizations
@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 Jan 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants