[Merged by Bors] - chore: rename `IsIntegralCurve` to `IsMIntegralCurve` by winstonyin · Pull Request #26563 · leanprover-community/mathlib4

winstonyin · 2025-06-30T23:23:05Z

I rename all the existing IsIntegralCurve series of definitions and lemmas for manifolds to IsMIntegralCurve in preparation for reusing IsIntegralCurve for the vector space version.

depends on: [Merged by Bors] - feat: fix definition of IsIntegralCurveOn for consistency #26533

github-actions · 2025-06-30T23:24:17Z

PR summary 84a77eea34

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsMIntegralCurve
+ IsMIntegralCurve.comp_add
+ IsMIntegralCurve.comp_mul
+ IsMIntegralCurve.continuous
+ IsMIntegralCurve.isMIntegralCurveAt
+ IsMIntegralCurve.isMIntegralCurveOn
+ IsMIntegralCurve.periodic_of_eq
+ IsMIntegralCurve.periodic_xor_injective
+ IsMIntegralCurveAt
+ IsMIntegralCurveAt.comp_add
+ IsMIntegralCurveAt.comp_mul_ne_zero
+ IsMIntegralCurveAt.continuousAt
+ IsMIntegralCurveAt.eventually_hasDerivAt
+ IsMIntegralCurveAt.hasMFDerivAt
+ IsMIntegralCurveAt.isMIntegralCurveOn
+ IsMIntegralCurveOn
+ IsMIntegralCurveOn.comp_add
+ IsMIntegralCurveOn.comp_mul
+ IsMIntegralCurveOn.continuousOn
+ IsMIntegralCurveOn.continuousWithinAt
+ IsMIntegralCurveOn.hasDerivWithinAt
+ IsMIntegralCurveOn.isMIntegralCurveAt
+ IsMIntegralCurveOn.mono
+ eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo
+ eqOn_of_isMIntegralCurveOn_Ioo
+ eqOn_piecewise_of_isMIntegralCurveOn_Ioo
+ exists_isMIntegralCurveAt_of_contMDiffAt
+ exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless
+ exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo
+ exists_isMIntegralCurve_of_isMIntegralCurveOn
+ isMIntegralCurveAt_comp_add
+ isMIntegralCurveAt_comp_mul_ne_zero
+ isMIntegralCurveAt_comp_sub
+ isMIntegralCurveAt_eventuallyEq_of_contMDiffAt
+ isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless
+ isMIntegralCurveAt_iff
+ isMIntegralCurveAt_iff'
+ isMIntegralCurveOn_Ioo_eqOn_of_contMDiff
+ isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless
+ isMIntegralCurveOn_comp_add
+ isMIntegralCurveOn_comp_mul_ne_zero
+ isMIntegralCurveOn_comp_sub
+ isMIntegralCurveOn_iff_isMIntegralCurveAt
+ isMIntegralCurveOn_piecewise
+ isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless
+ isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo
+ isMIntegralCurve_comp_add
+ isMIntegralCurve_comp_mul_ne_zero
+ isMIntegralCurve_comp_sub
+ isMIntegralCurve_const
+ isMIntegralCurve_eq_of_contMDiff
+ isMIntegralCurve_iff_isMIntegralCurveAt
+ isMIntegralCurve_iff_isMIntegralCurveOn
- IsIntegralCurveOn.hasDerivAt
- exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo
- isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless
- isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo

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

mathlib4-dependent-issues-bot · 2025-07-01T22:02:55Z

This PR/issue depends on:

~~[Merged by Bors] - feat: fix definition of IsIntegralCurveOn for consistency #26533~~
By Dependent Issues (🤖). Happy coding!

grunweg

I started reviewing, and then realised that you probably haven't merged master yet. Please do so, then I'll be happy to continue.

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

grunweg

One first comment: got until line 200 of Basic.lean. To be continued!

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

grunweg

So sorry for the delay. I found one more missing deprecation, otherwise everything looks good to me. Do you mind bumping the deprecation date to the current date? (Optional, if there'll be new lemmas taking up the old names anyway.)
maintainer delegate

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

github-actions · 2025-08-12T13:02:12Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

bryangingechen · 2025-08-12T13:13:06Z

bors d+

mathlib-bors · 2025-08-12T13:13:09Z

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

winstonyin · 2025-08-13T22:41:10Z

bors r+

I rename all the existing `IsIntegralCurve` series of definitions and lemmas for manifolds to `IsMIntegralCurve` in preparation for reusing `IsIntegralCurve` for the vector space version. - [x] depends on: #26533

mathlib-bors · 2025-08-13T22:53:01Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…munity#26563) I rename all the existing `IsIntegralCurve` series of definitions and lemmas for manifolds to `IsMIntegralCurve` in preparation for reusing `IsIntegralCurve` for the vector space version. - [x] depends on: leanprover-community#26533

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

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

winstonyin added 17 commits June 26, 2025 21:30

IsIntegralCurve -> IsMIntegralCurve

0079cac

fix import

692cc7f

basic

4a161e6

HasMFDerivAt -> HasMFDerivWithinAt

9c4ba63

deprecate

d7186b5

fix

ad82560

fix

6aca9d6

fix

0b74d28

Merge branch 'IsIntegralCurveOn_fix' into IsIntegralCurve

a4fe886

basic

4e199b5

minor

e6dea64

docs

2e119cb

overview

4761605

transform

be5ed4b

Mathlib.lean

9d0a98f

rename only

6522b52

deprecate

dfa7f33

winstonyin added the t-differential-geometry Manifolds etc label Jun 30, 2025

Mathlib.lean

d4fff7b

winstonyin mentioned this pull request Jun 30, 2025

feat: IsIntegralCurve for solutions to ODEs #26534

Closed

1 task

winstonyin changed the title ~~feat: rename IsIntegralCurve to IsMIntegralCurve~~ chore: rename IsIntegralCurve to IsMIntegralCurve Jun 30, 2025

grunweg self-assigned this Jun 30, 2025

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jun 30, 2025

grunweg reviewed Jul 2, 2025

View reviewed changes

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean Show resolved Hide resolved

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 2, 2025

Merge branch 'master' into IsMIntegralCurve

a874300

grunweg reviewed Jul 2, 2025

View reviewed changes

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean Outdated Show resolved Hide resolved

winstonyin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 2, 2025

deprecate

28e3e1b

grunweg reviewed Aug 12, 2025

View reviewed changes

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 12, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 12, 2025

winstonyin added 2 commits August 12, 2025 12:24

deprecate

51989bb

bump deprecate date

24e6a59

mathlib-bors bot changed the title ~~chore: rename IsIntegralCurve to IsMIntegralCurve~~ [Merged by Bors] - chore: rename IsIntegralCurve to IsMIntegralCurve Aug 13, 2025

mathlib-bors bot closed this Aug 13, 2025

winstonyin mentioned this pull request Aug 31, 2025

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

Closed

1 task

Conversation

winstonyin commented Jun 30, 2025 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 84a77eea34

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jul 1, 2025

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Aug 12, 2025

Uh oh!

bryangingechen commented Aug 12, 2025

Uh oh!

mathlib-bors bot commented Aug 12, 2025

Uh oh!

winstonyin commented Aug 13, 2025

Uh oh!

mathlib-bors bot commented Aug 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

winstonyin commented Jun 30, 2025 •

edited by grunweg

Loading

github-actions bot commented Jun 30, 2025 •

edited

Loading