Skip to content

[Merged by Bors] - feat: better junk value for fderivWithin at isolated points#7117

Closed
sgouezel wants to merge 5 commits intomasterfrom
SG_improve_fderiv
Closed

[Merged by Bors] - feat: better junk value for fderivWithin at isolated points#7117
sgouezel wants to merge 5 commits intomasterfrom
SG_improve_fderiv

Conversation

@sgouezel
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel commented Sep 12, 2023

Currently, when x is isolated in the set s, then fderivWithin k f s x can be anything. We modify the definition by ensuring that it is equal to 0 in this case. This ensures that the range of derivWithin is always contained in the closure of the span of the range of f.


Open in Gitpod

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 12, 2023
@sgouezel sgouezel added t-analysis Analysis (normed *, calculus) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Sep 14, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 14, 2023

This PR/issue depends on:

@jcommelin
Copy link
Copy Markdown
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 14, 2023
bors bot pushed a commit that referenced this pull request Sep 14, 2023
Currently, when `x` is isolated in the set `s`, then `fderivWithin k f s x` can be anything. We modify the definition by ensuring that it is equal to `0` in this case. This ensures that the range of `derivWithin` is always contained in the closure of the span of the range of `f`.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 14, 2023
Currently, when `x` is isolated in the set `s`, then `fderivWithin k f s x` can be anything. We modify the definition by ensuring that it is equal to `0` in this case. This ensures that the range of `derivWithin` is always contained in the closure of the span of the range of `f`.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: better junk value for fderivWithin at isolated points [Merged by Bors] - feat: better junk value for fderivWithin at isolated points Sep 14, 2023
@bors bors bot closed this Sep 14, 2023
@bors bors bot deleted the SG_improve_fderiv branch September 14, 2023 15:54
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
Currently, when `x` is isolated in the set `s`, then `fderivWithin k f s x` can be anything. We modify the definition by ensuring that it is equal to `0` in this case. This ensures that the range of `derivWithin` is always contained in the closure of the span of the range of `f`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants