Skip to content

[Merged by Bors] - feat: local frames in a vector bundle#30338

Closed
grunweg wants to merge 16 commits intoleanprover-community:masterfrom
grunweg:localframes-1
Closed

[Merged by Bors] - feat: local frames in a vector bundle#30338
grunweg wants to merge 16 commits intoleanprover-community:masterfrom
grunweg:localframes-1

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Oct 8, 2025 •
edited
Loading

We define a predicate IsLocalFrameOn, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section t w.r.t. a local frame, or proving smoothness of t via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot patrickmassot@free.fr

Open in Gitpod

@github-actions github-actions bot added the t-differential-geometry Manifolds etc label Oct 8, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 8, 2025 •
edited
Loading

PR summary c7bb7934b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (new file) 2101

Declarations diff

+ IsLocalFrameOn
+ coeff
+ coeff_apply_of_mem
+ coeff_apply_of_notMem
+ coeff_apply_zero_at
+ coeff_congr
+ coeff_eq_of_eq
+ coeff_sum_eq
+ congr
+ contMDiffAt
+ contMDiffAt_of_coeff
+ contMDiffAt_of_coeff_aux
+ contMDiffOn_of_coeff
+ eq_iff_coeff
+ eventually_eq_sum_coeff_smul
+ mdifferentiableAt_of_coeff
+ mdifferentiableAt_of_coeff_aux
+ mdifferentiableOn_of_coeff
+ mono
+ toBasisAt
+ toBasisAt_coe

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

@grunweg grunweg mentioned this pull request Oct 8, 2025
Closed
4 tasks
@grunweg grunweg mentioned this pull request Oct 8, 2025
Draft
35 tasks
ocfnash
ocfnash approved these changes Oct 20, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thanks, just a bunch of nitpicks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2025

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 20, 2025
@grunweg @ocfnash
Apply easy review comments
c630841 
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
grunweg
grunweg commented Oct 20, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor Author

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Thank you for the careful review. I'm still learning something new every time. I have some comments on your comments (and will fully address them once I'm out of my teaching cave for the week).

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Oct 22, 2025

Thank you for the quick and careful review!
bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 22, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 22, 2025
@grunweg
feat: local frames in a vector bundle (#30338)
f311695 
We define a predicate `IsLocalFrameOn`, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section `t` w.r.t. a local frame, or proving smoothness of `t` via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 22, 2025

This PR was included in a batch that was canceled, it will be automatically retried

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Oct 22, 2025

Looks like there's a long line:

https://github.com/leanprover-community/mathlib4/actions/runs/18731607041/job/53429667421#step:20:7059

bors r-

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 22, 2025

Canceled.

@ghost ghost removed ready-to-merge This PR has been sent to bors. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels Oct 22, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Oct 23, 2025

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 23, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 23, 2025
@grunweg
feat: local frames in a vector bundle (#30338)
8acb4f3 
We define a predicate `IsLocalFrameOn`, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section `t` w.r.t. a local frame, or proving smoothness of `t` via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 23, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: local frames in a vector bundle [Merged by Bors] - feat: local frames in a vector bundle Oct 23, 2025
@mathlib-bors mathlib-bors bot closed this Oct 23, 2025
@grunweg grunweg deleted the localframes-1 branch October 23, 2025 12:54
Jlh18 pushed a commit to Jlh18/mathlib4 that referenced this pull request Oct 24, 2025
@grunweg @Jlh18
feat: local frames in a vector bundle (leanprover-community#30338)
8193e87 
We define a predicate `IsLocalFrameOn`, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section `t` w.r.t. a local frame, or proving smoothness of `t` via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@grunweg @BeibeiX0
feat: local frames in a vector bundle (leanprover-community#30338)
7d4e65c 
We define a predicate `IsLocalFrameOn`, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section `t` w.r.t. a local frame, or proving smoothness of `t` via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
FormulaRabbit81 pushed a commit to FormulaRabbit81/mathlib4 that referenced this pull request Nov 8, 2025
@grunweg @FormulaRabbit81
feat: local frames in a vector bundle (leanprover-community#30338)
4894746 
We define a predicate `IsLocalFrameOn`, for a collection of sections of a vector bundle to be a local frame.
We provide some basic API, such as the coefficients of a section `t` w.r.t. a local frame, or proving smoothness of `t` via proving the smoothness of its local frame coefficients.

A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees

@hrmacbeth hrmacbeth

Labels

ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@grunweg @bryangingechen @ocfnash @hrmacbeth