feat(Topology/Order/Rolle): versions of Rolle's theorem for unbounded intervals

[ghost]

Mathlib's Rolle theorems all assume finite endpoints, in both the Icc form (exists_hasDerivAt_eq_zero) and the Ioo-with-equal-one-sided-limits form (exists_hasDerivAt_eq_zero'). This adds the unbounded analogues: if a function tends to the same limit at the two ends of Ioi a, of Iio b, or of the whole line, then it has a local extremum there, and hence a vanishing derivative.

Added to Mathlib/Topology/Order/Rolle.lean:

• exists_isExtrOn_Ioi_of_tendsto, exists_isLocalExtr_Ioi_of_tendsto
• exists_isExtrOn_Iio_of_tendsto, exists_isLocalExtr_Iio_of_tendsto
• exists_isExtrOn_univ_of_tendsto, exists_isLocalExtr_of_tendsto

and to Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean:

• exists_hasDerivAt_eq_zero_Ioi, exists_deriv_eq_zero_Ioi
• exists_hasDerivAt_eq_zero_Iio, exists_deriv_eq_zero_Iio
• exists_hasDerivAt_eq_zero_of_tendsto, exists_deriv_eq_zero_of_tendsto

Design notes

The topological lemmas are stated at the existing generality of Topology/Order/Rolle.lean rather than only for ℝ, which turned out to cost nothing: compactness of Icc is available from ConditionallyCompleteLinearOrder.toCompactIccSpace, the max/min case split is handled by instantiating a max-only private helper at (Y := Yᵒᵈ) — the idiom Topology/Order/Compact.lean already uses for Continuous.exists_forall_ge' — and the endpoint cutoffs come from mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset and eventually_atTop.

The price is three extra typeclass assumptions, needed only so that the intervals and atTop/atBot are non-degenerate and for the branch where f is identically l: [NoMaxOrder X] for Ioi, [NoMinOrder X] for Iio, [Nonempty X] for the whole space. ℝ satisfies all three by instance, so the six calculus corollaries are one-liners in the style of the existing exists_hasDerivAt_eq_zero'.

Three helpers are private; a reviewer may prefer the IsMaxOn/IsMinOn forms exposed, which is a mechanical change.

This is a prerequisite for a follow-up PR proving that the Hermite polynomials have n simple real roots, where the two outermost roots at each induction step are exactly the ones ordinary Rolle cannot produce.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary 96d42c99ee

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ exists_deriv_eq_zero_Iio
+ exists_deriv_eq_zero_Ioi
+ exists_deriv_eq_zero_of_tendsto
+ exists_hasDerivAt_eq_zero_Iio
+ exists_hasDerivAt_eq_zero_Ioi
+ exists_hasDerivAt_eq_zero_of_tendsto
+ exists_isExtrOn_Iio_of_tendsto
+ exists_isExtrOn_Ioi_of_tendsto
+ exists_isExtrOn_univ_of_tendsto
+ exists_isLocalExtr_Iio_of_tendsto
+ exists_isLocalExtr_Ioi_of_tendsto
+ exists_isLocalExtr_of_tendsto
+ exists_isMaxOn_Iio_of_tendsto
+ exists_isMaxOn_Ioi_of_tendsto
+ exists_isMaxOn_of_forall_lt
+ exists_isMaxOn_univ_of_tendsto

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 96d42c9).

• +12 new declarations
• −0 removed declarations

+exists_deriv_eq_zero_Iio
+exists_deriv_eq_zero_Ioi
+exists_deriv_eq_zero_of_tendsto
+exists_hasDerivAt_eq_zero_Iio
+exists_hasDerivAt_eq_zero_Ioi
+exists_hasDerivAt_eq_zero_of_tendsto
+exists_isExtrOn_Iio_of_tendsto
+exists_isExtrOn_Ioi_of_tendsto
+exists_isExtrOn_univ_of_tendsto
+exists_isLocalExtr_Iio_of_tendsto
+exists_isLocalExtr_Ioi_of_tendsto
+exists_isLocalExtr_of_tendsto

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 96d42c99ee
Reference commit 156b4fb350

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[ghost]

Withdrawing this PR at the request of the code owner; it was submitted without their authorization. Apologies for the noise.