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

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.

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

sgouezel · 2026-04-26T07:46:08Z

+open scoped ENNReal NNReal Topology ContDiff
+
+/-- A function `f : ℝ → ℝ` is absolutely monotone on a set `s` if it is smooth on `s` and all
+iterated derivatives within `s` are nonnegative. -/


This definition is not very good, because it forces you to have UniqueDiffOn assumptions in most statements. You should rather phrase it as: there exists a Taylor series for f on s whose terms are all nonnegative.

Thanks, you're right that the iteratedDerivWithin-based definition forces UniqueDiffOn everywhere and that's not needed. How about this:

def AbsolutelyMonotoneOn (f : ℝ → ℝ) (s : Set ℝ) : Prop := ∃ p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ, HasFTaylorSeriesUpToOn ∞ f p s ∧ ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ p x n fun _ => 1

There is one point which still requires UniqueDiffOn s, the proof that if f and g are both absolutely monotone on s, then f * g is absolutely monotone on s, which uses the Leibniz rule. This might be fixable with more work.

-awaiting-author

Yes, that sounds good. For the multiplication, this should still be ok with the new definition, but it would require a missing lemma in Mathlib, saying that if two functions have Taylor series then the product also has a Taylor series given by the Leibniz formula. That's one of the points of these formalizations with the right assumptions, finding things that should be improved in the library.

sgouezel · 2026-04-26T07:47:05Z

When you are done with a conversation, could you close it? This helps focus on the remaining points.

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

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

vihdzp reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

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

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

Comment thread Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean Outdated

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

sgouezel reviewed Apr 26, 2026

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 26, 2026

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!

Uh oh!

Uh oh!

Uh oh!

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!

Uh oh!

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!

sgouezel Apr 26, 2026

Choose a reason for hiding this comment

Uh oh!

mrdouglasny Apr 26, 2026

Choose a reason for hiding this comment

Uh oh!

mrdouglasny Apr 26, 2026

Choose a reason for hiding this comment

Uh oh!

sgouezel Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

sgouezel commented Apr 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

github-actions Bot commented Apr 14, 2026 •

edited

Loading