feat(Analysis/Calculus): define absolutely monotone functions by mrdouglasny · Pull Request #38026 · leanprover-community/mathlib4

mrdouglasny · 2026-04-14T03:10:01Z

Summary

Define AbsolutelyMonotoneOn f s for functions f : ℝ → ℝ that are smooth on s with all iterated derivatives within s nonneg
Prove closure under add, smul, mul
Show exp, cosh, constants, and powers are absolutely monotone on appropriate domains

This is the first part of a split of #37879. Follow-up PRs will add:

Bernstein backward direction (nonneg coefficients → absolutely monotone)
Bernstein forward direction (absolutely monotone → analytic at 0)
Matrix applications (Schur product theorem for power series, entrywise exp)

Test plan

CI passes (build + lint)
Verify AbsolutelyMonotoneOn structure and examples type-check

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.6 (1M context) noreply@anthropic.com

Define `AbsolutelyMonotoneOn f s` for functions with nonneg iterated derivatives within a set. Prove closure under addition, scalar multiplication, and multiplication, plus show exp, cosh, constants, and powers are absolutely monotone on appropriate domains. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

github-actions · 2026-04-14T03:10:13Z

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 · 2026-04-14T03:11:07Z

PR summary 2ff88851d5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Calculus.AbsolutelyMonotone` (new file)	1802

Declarations diff

+ AbsolutelyMonotoneOn
+ add
+ mul
+ of_contDiff
+ smul

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

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

vihdzp · 2026-04-14T03:16:50Z

+# Absolutely Monotone Functions
+
+A function `f : ℝ → ℝ` is absolutely monotone on a set `s` if it is smooth
+on `s` and all its iterated derivatives within `s` are nonneg on `s`.


Suggested change

on `s` and all its iterated derivatives within `s` are nonneg on `s`.

on `s` and all its iterated derivatives within `s` are nonnegative on `s`.

vihdzp · 2026-04-14T03:19:27Z

+    exact h n x hx
+
+/-- Nonneg Taylor coefficients at any point in `s`. -/
+theorem nonneg_taylor_coeffs {f : ℝ → ℝ} {s : Set ℝ}


This seems redundant to me, since it follows immediately from 0 ≤ iteratedDerivWithin n f s x.

vihdzp · 2026-04-14T03:23:40Z

+
+end AbsolutelyMonotoneOn
+
+/-! ### Examples -/


I think these examples should go in separate files. This definition shouldn't require Real.cosh in order to be imported, for instance.

vihdzp · 2026-04-14T03:24:23Z

+    simp only [iteratedDeriv_const]
+    split
+    · exact hc
+    · exact le_refl 0


Suggested change

· exact le_refl 0

· rfl

wwylele · 2026-04-14T03:25:09Z

Could you format the code to fill up the 100-character limit per line?
(Why is this a recurring problem from Claude code? This should be trivial to solve, either by human or AI)

- "nonneg" → "nonnegative" in docstrings - Remove redundant `nonneg_taylor_coeffs` - Move examples (exp, cosh, const, pow) out to avoid pulling heavy imports — they will go in a follow-up file - Fill lines to 100-char limit - Trim unused imports (only IteratedDeriv.Lemmas needed for def + closure) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

j-loreaux · 2026-04-15T05:04:11Z

I know very little about absolutely monotone functions and what are the correct design choices, so I am going to remove my assignment on this PR. Maybe @sgouezel wants to take it up?

j-loreaux

This looks reasonable to me, but it not my area of expertise.

j-loreaux · 2026-04-15T05:05:54Z

+
+## References
+
+* Widder, D.V. (1941). *The Laplace Transform*.


This should be added to the .bib file as an actual reference, and linked here.

Maybe worth double-checking it isn't an AI hallucinated reference.

j-loreaux · 2026-04-15T05:10:43Z

+/-- Constructor from global `ContDiff` and global `iteratedDeriv`. Works for any `UniqueDiffOn`
+set (includes open sets, `Ici a`, convex sets with nonempty interior, etc.). -/


Suggested change

/-- Constructor from global `ContDiff` and global `iteratedDeriv`. Works for any `UniqueDiffOn`

set (includes open sets, `Ici a`, convex sets with nonempty interior, etc.). -/

/-- A globally smooth function all of whose iterated derivatives are nonnegative on a set `s`

satisfying `UniqueDiffOn` is absolutely monotone on `s`. Such sets `s` include open sets,

`Set.Ici`, and convex sets with nonempty interior. -/

- Add Widder, *The Laplace Transform* (1941) to references.bib and link via bibkey in the module doc - Clarify `of_contDiff` docstring (vs generic "Constructor from ...") Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

lint-bib.sh uses bibtool case-insensitive sort — lowercase 'widder' comes before 'Wielandt', not after. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

mrdouglasny · 2026-04-16T02:00:56Z

Addressed all review comments:

Examples split out: exp, cosh, pow, const, and Bernstein theorems removed from this PR (will go in a follow-up)
Widder reference: added widder1941 entry to references.bib and linked in the docstring
Line wrapping: reformatted to 100-char limit
Docstrings: applied suggested rewording (nonneg to nonnegative, expanded of_contDiff docstring)
Redundant lemma: removed nonneg_taylor_coeffs

Re: the Widder reference -- it is real, not hallucinated: The Laplace Transform by David V. Widder (1941) on Amazon

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

mrdouglasny · 2026-04-19T01:14:22Z

All reviewer comments have been addressed. Could a maintainer please remove the awaiting-author label? Thanks.

wwylele · 2026-04-19T03:24:16Z

You can remove it yourself by typing "-awaiting-author". For more information about PR lifecycle, you can read https://leanprover-community.github.io/contribute/index.html

mrdouglasny · 2026-04-19T05:27:58Z

-awaiting-author

ADedecker · 2026-04-23T11:44:25Z

Sorry, I am going to remove my assignment because I would rather dedicate my scarce reviewing time to human-written code.

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 14, 2026

github-actions Bot added the t-analysis Analysis (normed *, calculus) label Apr 14, 2026

vihdzp reviewed Apr 14, 2026

View reviewed changes

themathqueen added the LLM-generated PRs with substantial input from LLMs - review accordingly label Apr 14, 2026

mathlib-triage Bot assigned j-loreaux Apr 15, 2026

j-loreaux removed their assignment Apr 15, 2026

j-loreaux reviewed Apr 15, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 15, 2026

mrdouglasny and others added 2 commits April 15, 2026 01:56

refactor: address j-loreaux review comments

f7ded8d

- Add Widder, *The Laplace Transform* (1941) to references.bib and link via bibkey in the module doc - Clarify `of_contDiff` docstring (vs generic "Constructor from ...") Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

fix: move widder1941 to correct alphabetical position

6ad343f

lint-bib.sh uses bibtool case-insensitive sort — lowercase 'widder' comes before 'Wielandt', not after. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

style: wrap all lines to ≤100 characters in AbsolutelyMonotone

fb78495

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 19, 2026

mathlib-triage Bot assigned ADedecker Apr 22, 2026

ADedecker removed their assignment Apr 23, 2026

mathlib-triage Bot assigned sgouezel Apr 25, 2026

	on `s` and all its iterated derivatives within `s` are nonneg on `s`.
	on `s` and all its iterated derivatives within `s` are nonnegative on `s`.


		## References

		* Widder, D.V. (1941). The Laplace Transform.

		/-- Constructor from global `ContDiff` and global `iteratedDeriv`. Works for any `UniqueDiffOn`
		set (includes open sets, `Ici a`, convex sets with nonempty interior, etc.). -/

-/-- Constructor from global `ContDiff` and global `iteratedDeriv`. Works for any `UniqueDiffOn`
-set (includes open sets, `Ici a`, convex sets with nonempty interior, etc.). -/
+/-- A globally smooth function all of whose iterated derivatives are nonnegative on a set `s`
+satisfying `UniqueDiffOn` is absolutely monotone on `s`. Such sets `s` include open sets,
+`Set.Ici`, and convex sets with nonempty interior. -/

Conversation

mrdouglasny commented Apr 14, 2026

Summary

Test plan

Uh oh!

github-actions Bot commented Apr 14, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2ff88851d5

Import changes for modified files

Declarations diff

Uh oh!

vihdzp Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

wwylele commented Apr 14, 2026

Uh oh!

j-loreaux commented Apr 15, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 16, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

mrdouglasny commented Apr 16, 2026

Uh oh!

mrdouglasny commented Apr 19, 2026

Uh oh!

wwylele commented Apr 19, 2026

Uh oh!

mrdouglasny commented Apr 19, 2026

Uh oh!

ADedecker commented Apr 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

github-actions Bot commented Apr 14, 2026 •

edited

Loading