Skip to content

[Merged by Bors] - feat: IsIntegralCurve for solutions to ODEs#29186

Closed
winstonyin wants to merge 27 commits intoleanprover-community:masterfrom
winstonyin:ODE_IsIntegralCurve
Closed

[Merged by Bors] - feat: IsIntegralCurve for solutions to ODEs#29186
winstonyin wants to merge 27 commits intoleanprover-community:masterfrom
winstonyin:ODE_IsIntegralCurve

Conversation

@winstonyin
Copy link
Copy Markdown
Collaborator

@winstonyin winstonyin commented Aug 31, 2025 •
edited
Loading

I define IsIntegralCurve etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels IsMIntegralCurve etc. for manifolds.

Moved from #26534.

Open in Gitpod

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Aug 31, 2025
@winstonyin winstonyin mentioned this pull request Aug 31, 2025
Closed
1 task
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 31, 2025 •
edited
Loading

PR summary 332fc33e62

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.ODE.Basic (new file) 1654
Mathlib.Analysis.ODE.Transform (new file) 1768

Declarations diff

+ IsIntegralCurve
+ IsIntegralCurve.comp_add
+ IsIntegralCurve.comp_mul
+ IsIntegralCurve.comp_sub
+ IsIntegralCurve.continuous
+ IsIntegralCurve.isIntegralCurveAt
+ IsIntegralCurve.isIntegralCurveOn
+ IsIntegralCurveAt
+ IsIntegralCurveAt.comp_add
+ IsIntegralCurveAt.comp_mul_ne_zero
+ IsIntegralCurveAt.comp_sub
+ IsIntegralCurveAt.continuousAt
+ IsIntegralCurveAt.hasDerivAt
+ IsIntegralCurveAt.isIntegralCurveOn
+ IsIntegralCurveOn
+ IsIntegralCurveOn.comp_add
+ IsIntegralCurveOn.comp_mul
+ IsIntegralCurveOn.comp_sub
+ IsIntegralCurveOn.continuousOn
+ IsIntegralCurveOn.continuousWithinAt
+ IsIntegralCurveOn.isIntegralCurveAt
+ IsIntegralCurveOn.mono
+ isIntegralCurveAt_comp_add
+ isIntegralCurveAt_comp_mul_ne_zero
+ isIntegralCurveAt_comp_sub
+ isIntegralCurveAt_iff_exists_mem_nhds
+ isIntegralCurveAt_iff_exists_pos
+ isIntegralCurveOn_comp_add
+ isIntegralCurveOn_comp_mul_ne_zero
+ isIntegralCurveOn_comp_sub
+ isIntegralCurveOn_iff_isIntegralCurveAt
+ isIntegralCurveOn_univ
+ isIntegralCurve_comp_add
+ isIntegralCurve_comp_mul_ne_zero
+ isIntegralCurve_comp_sub
+ isIntegralCurve_const
+ isIntegralCurve_iff_isIntegralCurveAt

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

@winstonyin winstonyin added t-differential-geometry Manifolds etc t-dynamics Dynamical Systems labels Aug 31, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Aug 31, 2025

This PR/issue depends on:

@grunweg grunweg mentioned this pull request Aug 31, 2025
Open
3 tasks
@grunweg grunweg self-assigned this Oct 28, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

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

@github-actions 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 Nov 27, 2025
@grunweg grunweg removed their assignment Nov 27, 2025
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Nov 27, 2025

While I care about this PR getting merged, realistically I cannot commit to reviewing it within the next three weeks - so I'm unassigning myself. Thanks for making the PR and your great patience; I hope this can still get merged soon.

sgouezel
sgouezel reviewed Nov 28, 2025
View reviewed changes
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 4, 2025
@winstonyin winstonyin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 10, 2025
@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 30, 2026
sgouezel
sgouezel reviewed Feb 1, 2026
View reviewed changes
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 1, 2026
@winstonyin winstonyin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 3, 2026
@michaellee94 michaellee94 requested a review from sgouezel February 3, 2026 18:53
@michaellee94
Copy link
Copy Markdown
Collaborator

michaellee94 commented Feb 3, 2026 •
edited
Loading

Thanks for reviewing this PR, @sgouezel! Hoping to rebase #26413 on top of this.

@winstonyin winstonyin mentioned this pull request Feb 9, 2026
Open
1 task
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 18, 2026

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

@mathlib-merge-conflicts 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 Feb 18, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts 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 Feb 20, 2026
@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 28, 2026
@winstonyin winstonyin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 2, 2026
sgouezel
sgouezel reviewed Mar 13, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+
Thanks!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 13, 2026

✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 13, 2026
@winstonyin
Copy link
Copy Markdown
Collaborator Author

winstonyin commented Mar 20, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 20, 2026
@winstonyin
feat: IsIntegralCurve for solutions to ODEs (#29186)
ec6dab0 
I define `IsIntegralCurve` etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels `IsMIntegralCurve` etc. for manifolds.

Moved from #26534.

- [x] depends on: #26563
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 20, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: IsIntegralCurve for solutions to ODEs [Merged by Bors] - feat: IsIntegralCurve for solutions to ODEs Mar 20, 2026
@mathlib-bors mathlib-bors bot closed this Mar 20, 2026
justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Mar 28, 2026
@winstonyin @justus-springer
feat: IsIntegralCurve for solutions to ODEs (leanprover-community#29186)
181bea4 
I define `IsIntegralCurve` etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels `IsMIntegralCurve` etc. for manifolds.

Moved from leanprover-community#26534.

- [x] depends on: leanprover-community#26563
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

@mcdoll mcdoll mcdoll left review comments

Assignees

@sgouezel sgouezel

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus) t-differential-geometry Manifolds etc t-dynamics Dynamical Systems

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@winstonyin @mathlib4-dependent-issues-bot @mathlib4-merge-conflict-bot @grunweg @mcdoll @michaellee94 @sgouezel @jcommelin