PR summary b9c0430677

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

This PR/issue depends on:

• [Merged by Bors] - feat: add a positivity extension for Real.toNNReal #31956
• [Merged by Bors] - feat(MetricSpace): images and preimages of balls in subtypes #31957
  By Dependent Issues (🤖). Happy coding!

This pull request has conflicts, please merge master and resolve them.

Could you please comment on what you want to do with this lemma? It is pretty mysterious to me. Is it part of your Sard effort?

For Sard's Theorem, I need a weaker version of this theorem, namely that this lower bound exists for each normed space. If we decide to merge this theorem too, then we can make some intermediate estimate depend on the dimension of the domain only, but it turned out to be not necessary for the proof.

Here is the estimate I need it for. If a is a density point of the set {x | fderiv Real f x = 0}, then fderiv Real f x = O(x^r) as x → a implies not only f x - f a = O(x ^ (r + 1)), but f x - f a = o(x ^ (r + 1)). This lemma would allow us to turn this o into a precise estimate based on the part of ball a (dist x a) occupied by zeros of the derivative and the constant in fderiv Real f x = O(x^r). As I said above, this turned out to be not required for the main result.

I formalized this version, because Moreira explicitly claims that the estimate is uniform, and it seemed to be important later, before I slightly changed the argument. I'm OK with leaving this version as a leftover in SardMoreira.

I’m sorry I forgot about that. I guess we can keep it anyway.
bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step