feat(MonotoneConvergence): strict versions of ge_of_tendsto

[seewoo5]

---

Strict versions of Monotone.ge_of_tendsto and similar theorems: StrictMono.gt_of_tendsto, StrictMono.lt_of_tendsto, StrictAnti.lt_of_tendsto, StrictAnti.gt_of_tendsto. These require extra hypothesis such as NoMaxOrder β or NoMinOrder β. Claude is used to find the hypothesis and write initial proofs.

Context: In Sphere packing project, there is an inequality of the form $f(t) < L$ for a strictly decreasing function $f$ on $(0, \infty)$ with $\lim_{t \to 0^+} f(t) = L$. Currently, this is proved by $f(t) < f(t/2) \le L$, where the last step uses ge_of_tendsto. With new theorems in this PR, we don't need to consider $f(t/2)$ anymore (by using StrictAnti.gt_of_tendsto).

[github-actions]

PR summary c152791ca0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ StrictAnti.gt_of_tendsto
+ StrictAnti.lt_of_tendsto
+ StrictMono.gt_of_tendsto
+ StrictMono.lt_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 c152791).

• +4 new declarations
• −0 removed declarations

+StrictAnti.gt_of_tendsto
+StrictAnti.lt_of_tendsto
+StrictMono.gt_of_tendsto
+StrictMono.lt_of_tendsto

---

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

Current commit c152791ca0
Reference commit b0df0c4b5c

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