Skip to content

[Merged by Bors] - feat: mdifferentiableOn_section_of_mem_baseSet₀#26870

Closed
grunweg wants to merge 6 commits intoleanprover-community:masterfrom
grunweg:mdifferentiableOn_membaseset
Closed

[Merged by Bors] - feat: mdifferentiableOn_section_of_mem_baseSet₀#26870
grunweg wants to merge 6 commits intoleanprover-community:masterfrom
grunweg:mdifferentiableOn_membaseset

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 7, 2025 •
edited
Loading

The MDifferentiable analogue of contMDiffOn_section_of_mem_baseSet₀.
From the path towards geodesics and the Levi-Civita connection.

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

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 7, 2025 •
edited
Loading

PR summary c728e645fc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ MDifferentiableWithinAt.change_section_trivialization
+ Trivialization.contMDiffAt_section_iff
+ Trivialization.contMDiffOn_section_baseSet_iff
+ Trivialization.contMDiffOn_section_iff
+ Trivialization.mdifferentiableAt_section_iff
+ Trivialization.mdifferentiableAt_snd_comp_iff₂
+ Trivialization.mdifferentiableAt_totalSpace_iff
+ Trivialization.mdifferentiableOn_section_baseSet_iff
+ Trivialization.mdifferentiableOn_section_iff
+ Trivialization.mdifferentiableWithinAt_section_iff
+ Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
+ Trivialization.mdifferentiableWithinAt_totalSpace_iff

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

@github-actions github-actions bot added the t-differential-geometry Manifolds etc label Jul 7, 2025
@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 Jul 7, 2025
This was referenced Jul 7, 2025
Draft
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 7, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 7, 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 Jul 16, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jul 16, 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 Jul 17, 2025
@grunweg grunweg force-pushed the mdifferentiableOn_membaseset branch from 769f230 to 241e1ee Compare July 17, 2025 13:25
@grunweg grunweg assigned sgouezel and unassigned PatrickMassot Aug 22, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 22, 2025 •
edited
Loading

Unassigning Patrick (he's a co-author, the automated algorithm does not take this into account).
@sgouezel Would you like to review this one? This one should be straightforward, the result is analogous to a result about ContMDiff. (I've mentioned this in the PR description now.)

sgouezel
sgouezel reviewed Sep 15, 2025
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 Sep 15, 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 Sep 15, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Sep 15, 2025

Thank you for the review!
bors merge

mathlib-bors bot pushed a commit that referenced this pull request Sep 15, 2025
@grunweg @PatrickMassot
feat: mdifferentiableOn_section_of_mem_baseSet₀ (#26870)
9ccb6e7 
The `MDifferentiable` analogue of `contMDiffOn_section_of_mem_baseSet₀`.
From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 15, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: mdifferentiableOn_section_of_mem_baseSet₀ [Merged by Bors] - feat: mdifferentiableOn_section_of_mem_baseSet₀ Sep 15, 2025
@mathlib-bors mathlib-bors bot closed this Sep 15, 2025
@grunweg grunweg deleted the mdifferentiableOn_membaseset branch September 15, 2025 19:54
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@grunweg @PatrickMassot @joelriou
feat: mdifferentiableOn_section_of_mem_baseSet₀ (leanprover-community…
e7f7b00 
…#26870)

The `MDifferentiable` analogue of `contMDiffOn_section_of_mem_baseSet₀`.
From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
zhuyizheng pushed a commit to zhuyizheng/mathlib4 that referenced this pull request Oct 2, 2025
@grunweg @PatrickMassot @zhuyizheng
feat: mdifferentiableOn_section_of_mem_baseSet₀ (leanprover-community…
cceb47b 
…#26870)

The `MDifferentiable` analogue of `contMDiffOn_section_of_mem_baseSet₀`.
From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
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

Assignees

@sgouezel sgouezel

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @leanprover-community-bot-assistant @mathlib4-dependent-issues-bot @sgouezel @PatrickMassot