Skip to content

feat: IsIntegralCurve for solutions to ODEs#26534

Closed
winstonyin wants to merge 25 commits intoleanprover-community:masterfrom
winstonyin:IsIntegralCurve
Closed

feat: IsIntegralCurve for solutions to ODEs#26534
winstonyin wants to merge 25 commits intoleanprover-community:masterfrom
winstonyin:IsIntegralCurve

Conversation

@winstonyin
Copy link
Copy Markdown
Collaborator

@winstonyin winstonyin commented Jun 30, 2025 •
edited
Loading

Moved to #29186.

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.

Question for reviewers: how should I state the deprecation notice?

Open in Gitpod

@winstonyin winstonyin added t-analysis Analysis (normed *, calculus) t-dynamics Dynamical Systems t-differential-geometry Manifolds etc labels Jun 30, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2025 •
edited
Loading

PR summary 3887a9b6a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/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 mentioned this pull request Jun 30, 2025
Open
3 tasks
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 30, 2025
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 30, 2025

Question for reviewers: how should I state the deprecation notice?

Good question! As I understand it, we don't have a good way to deal with renames "B -> A, A -> B" or "B -> C; add B". If nothing else depends on it, one can stagger this a bit (e.g., land B -> C, wait for a new stable release, then land new lemmas B) --- but this is not done systematically at all.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 30, 2025

Given that this blocks #26413, waiting seems like a non-ideal option. You definitely don't have to do this!

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 30, 2025

In terms of reviewing, this would be slightly easier to review if split in two --- one PR for just the renames (perhaps adding deprecations for everything), and then a second PR with the new added files (which can delete deprecation aliasses which are now taken). The renames themselves are quick to review.
Would doing this split be acceptable for you?

@winstonyin
Copy link
Copy Markdown
Collaborator Author

winstonyin commented Jun 30, 2025

The two-PR solution works. Thanks!

@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 Aug 13, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 13, 2025

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

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 13, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

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

This PR/issue depends on:

@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 Aug 14, 2025
@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Aug 26, 2025

Something's wrong here: the PR branch is empty – can you fix it, or close the PR if all its content has already been added elsewhere?

@loefflerd loefflerd added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 26, 2025
@winstonyin
Revert "Merge branch 'master' into IsIntegralCurve"
8b9c163 
This reverts commit 96bb722, reversing
changes made to a874300.
@winstonyin
Revert "Merge branch 'master' into IsMIntegralCurve"
ff08b47 
This reverts commit a874300, reversing
changes made to d4fff7b.
@winstonyin
Revert "Mathlib.lean"
a6365cb 
This reverts commit d4fff7b.
@winstonyin
Revert "deprecate"
f608543 
This reverts commit dfa7f33.
@winstonyin
Revert "rename only"
7464085 
This reverts commit 6522b52.
@github-actions github-actions 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 Aug 31, 2025
@winstonyin winstonyin mentioned this pull request Aug 31, 2025
Closed
1 task
@winstonyin
Copy link
Copy Markdown
Collaborator Author

winstonyin commented Aug 31, 2025

@grunweg @loefflerd I moved to a new PR (#29186) because I'm bad at git...

@winstonyin winstonyin closed this Aug 31, 2025
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
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

No reviews

Assignees

@sgouezel sgouezel

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) 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.

6 participants

@winstonyin @grunweg @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot @loefflerd @sgouezel