[Merged by Bors] - feat(Analysis/ODE): add discrete Grönwall inequality by dennj · Pull Request #34709 · leanprover-community/mathlib4

dennj · 2026-02-02T03:56:28Z

Summary

Add discrete Grönwall inequality to Mathlib/Analysis/ODE/DiscreteGronwall.lean

Provides bounds for recurrence inequalities of the form u(n+1) ≤ c(n) * u(n) + b(n)

Main results

discrete_gronwall_prod_general: Product form working over any linearly ordered commutative ring
discrete_gronwall: Classical exponential bound u(n) ≤ (u(n₀) + ∑ b(k)) * exp(∑ c(i)) (ℝ-specific)
discrete_gronwall_Ico: Uniform bound over a finite interval (ℝ-specific)

Related work

Complements the continuous Grönwall inequality in Mathlib.Analysis.ODE.Gronwall

References

Grönwall, T. H. (1919). "Note on the derivatives with respect to a parameter of the solutions of a system of differential equations". Annals of Mathematics, 20(4), 292–296.

This is human-made PR with AI help in golfing proof and documenting the code.

github-actions · 2026-02-02T03:57:42Z

PR summary 977f84bd6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.ODE.DiscreteGronwall` (new file)	1920

Declarations diff

+ discrete_gronwall
+ discrete_gronwall_Ico
+ discrete_gronwall_prod_general

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.

No changes to technical debt.

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

grunweg · 2026-03-16T14:54:56Z

Hello from triage! My impression is that this PR was generated with substantial help from LLM. Can you comment on this, please? Per our AI policy, also mention this in the PR description.

j-loreaux

Long story short: grind is your friend.

Can you please answer the question about whether this PR is generated or assisted by AI?

mathlib-merge-conflicts · 2026-03-20T21:56:22Z

This pull request has conflicts, please merge master and resolve them.

euprunin · 2026-04-11T07:45:36Z

@dennj

Are you familiar with the merely-true project (https://github.com/merely-true/merely-true)? It's intended as a playground for LLM-generated mathematics, with very permissive contribution guidelines.

I'm not a Mathlib reviewer or maintainer, so I don't speak for the project, but I thought I'd mention it as a potentially interesting place for work like this (independently of how this PR is evaluated here).

dennj · 2026-04-27T00:27:53Z

-awaiting-author

I applied the suggestions in the comments and did some golfing

j-loreaux

Because this PR existed and I started reviewing it before the policy was enacted, I will not close this PR. But I want to draw your attention to our AI policy.

j-loreaux · 2026-04-28T14:05:04Z

+        add_le_add le_rfl <| sum_le_sum fun j hj ↦ mul_le_mul_of_nonneg_left
+          (prod_le_prod_of_subset_of_one_le
+            (Ico_subset_Ico_left (by have := mem_Ico.mp hj; omega))
+            (fun i hi ↦ by
+              have := mem_Ico.mp hj; have := mem_Ico.mp hi; linarith [hc i (by omega)])
+            (fun i hi _ ↦ by linarith [hc i (mem_Ico.mp hi).1]))
+          (hb j (mem_Ico.mp hj).1)


This proof is really unpleasant. There is a good reason I factored out this step in an earlier comment (which I now can't easily reference since you force-pushed to this branch, please don't do that). Please implement the suggestion I had before.

Thanks for the feedback.
I think I fixed the problem in the new commit.

j-loreaux · 2026-04-28T21:11:09Z

bors merge

## Summary Add discrete Grönwall inequality to `Mathlib/Analysis/ODE/DiscreteGronwall.lean` Provides bounds for recurrence inequalities of the form `u(n+1) ≤ c(n) * u(n) + b(n)` ### Main results - `discrete_gronwall_prod_general`: Product form working over any linearly ordered commutative ring - `discrete_gronwall`: Classical exponential bound `u(n) ≤ (u(n₀) + ∑ b(k)) * exp(∑ c(i))` (ℝ-specific) - `discrete_gronwall_Ico`: Uniform bound over a finite interval (ℝ-specific) ## Related work Complements the continuous Grönwall inequality in `Mathlib.Analysis.ODE.Gronwall` ## References * Grönwall, T. H. (1919). "Note on the derivatives with respect to a parameter of the solutions of a system of differential equations". *Annals of Mathematics*, 20(4), 292–296. This is human-made PR with AI help in golfing proof and documenting the code.

mathlib-bors · 2026-04-28T22:04:48Z

Build failed (retrying...):

ci (staging) / Build

## Summary Add discrete Grönwall inequality to `Mathlib/Analysis/ODE/DiscreteGronwall.lean` Provides bounds for recurrence inequalities of the form `u(n+1) ≤ c(n) * u(n) + b(n)` ### Main results - `discrete_gronwall_prod_general`: Product form working over any linearly ordered commutative ring - `discrete_gronwall`: Classical exponential bound `u(n) ≤ (u(n₀) + ∑ b(k)) * exp(∑ c(i))` (ℝ-specific) - `discrete_gronwall_Ico`: Uniform bound over a finite interval (ℝ-specific) ## Related work Complements the continuous Grönwall inequality in `Mathlib.Analysis.ODE.Gronwall` ## References * Grönwall, T. H. (1919). "Note on the derivatives with respect to a parameter of the solutions of a system of differential equations". *Annals of Mathematics*, 20(4), 292–296. This is human-made PR with AI help in golfing proof and documenting the code.

mathlib-bors · 2026-04-28T23:23:41Z

Pull request successfully merged into master.

Build succeeded:

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) labels Feb 2, 2026

mathlib-triage Bot assigned ADedecker Feb 6, 2026

mathlib-triage Bot assigned j-loreaux and unassigned ADedecker Mar 11, 2026

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026

j-loreaux reviewed Mar 20, 2026

View reviewed changes

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

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 20, 2026

dennj force-pushed the feat/discrete-gronwall branch from 5439f72 to 1015cc2 Compare April 27, 2026 00:20

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 27, 2026

feat: add discrete gronwall

099dcf6

dennj force-pushed the feat/discrete-gronwall branch from 1015cc2 to 099dcf6 Compare April 27, 2026 00:25

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

j-loreaux reviewed Apr 28, 2026

View reviewed changes

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

refactor(Analysis/ODE/DiscreteGronwall): generalize and golf

e042196

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

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Apr 28, 2026

mathlib-bors Bot changed the title ~~feat(Analysis/ODE): add discrete Grönwall inequality~~ [Merged by Bors] - feat(Analysis/ODE): add discrete Grönwall inequality Apr 28, 2026

mathlib-bors Bot closed this Apr 28, 2026

Conversation

dennj commented Feb 2, 2026 • edited by j-loreaux Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Main results

Related work

References

Uh oh!

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

Uh oh!

PR summary 977f84bd6e

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Mar 16, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Mar 20, 2026

Uh oh!

euprunin commented Apr 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dennj commented Apr 27, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

dennj Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux commented Apr 28, 2026

Uh oh!

mathlib-bors Bot commented Apr 28, 2026

Uh oh!

mathlib-bors Bot commented Apr 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

dennj commented Feb 2, 2026 •

edited by j-loreaux

Loading

github-actions Bot commented Feb 2, 2026 •

edited

Loading

euprunin commented Apr 11, 2026 •

edited

Loading