feat(Analysis/Calculus): monotonicity from nonnegative lower right Dini derivative outside a countable set

[benjub]

Prove that a real function which is continuous on a real interval and whose lower right Dini derivative is nonnegative outside a countable set is monotone, as well as its special case when the interval is the whole real line.

---

That is Proposition 2 in Bourbaki, Functions of a Real Variable, Ch. I, §2.2. The Lean proof follows closely Bourbaki's: the main differences are: adaptation to the MonotoneOn predicate on an interval, adaptation to weakening the hypothesis to an inequality on the lower right Dini derivative instead of the right derivative, and use of "some summable positive family" on the countable set instead of "choosing an enumeration a_n and assigning weight 2^{-n} to a_n").

Since mathlib currently has no definitions for Dini derivatives, I wrote the hypotheses using filters, as done in Mathlib/Analysis/Calculus/MeanValue.lean.

This result is close to the results in Mathlib/Analysis/Calculus/MeanValue.lean, but allows a countable singular set where the hypothesis on the lower right Dini derivatives need not hold. As indicated in a comment in the proof, the "continuous-induction lemmas" in Mathlib/Topology/Order/IntermediateValue.lean do not apply here, and another method is used.

I was unsure where to put this result: either in Mathlib/Analysis/Calculus/MeanValue.lean or in a new file in Mathlib/Analysis/Calculus/. I chose the latter, but I would welcome suggestions on the appropriate location or filename.

In future PRs, I could add variants: hypotheses on left Dini derivatives, conclusions using the predicates Antitone(On), StrictMono(On), vector-valued functions... Another generalization that was my original goal is to generalize variants of "strictly differentiable at a point iff derivative is continuous at that point", as well as to generalize to higher dimensions of the domain, where using Sard's theorem, the singular set can probably be any countable union of positive-codimensional embedded C^1 submanifolds (union sets of codimension at least 2).

Use of AI: I used ChatGPT mainly as an aid to locate existing lemmas that I needed in the proof (which is for me currently the hardest part of writing proofs). Once I had a compiling proof, I used Codex to suggest some linting, uniformizing, and name changes to conform more closely to mathlib conventions. That did not impact the structure of the proof, which I kept very close to Bourbaki's.

[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 https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary ebf4dbbefb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.MeanValueCountableExceptions (new file)	1489

---

Declarations diff (regex)

+ monotoneOn_of_liminf_slope_right_nonneg
+ monotone_of_liminf_slope_right_nonneg

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 -- unavailable)

⚠️ The Mathlib cache for this PR's merge-base isn't on the server (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit ebf4dbbefb
Reference commit e3b73828b0

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.sh 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).