[Merged by Bors] - feat(Manifold/PartitionOfUnity): existence of global C^n smooth section for nontrivial bundles#26875
Conversation
|
This PR continues #24966 |
PR summary 29cc0b6ba0
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.PartitionOfUnity | 2309 | 2317 | +8 (+0.35%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.WhitneyEmbedding |
1 |
3 filesMathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Geometry.Manifold.PartitionOfUnity |
8 |
Declarations diff
+ contMDiff_totalSpace_weighted_sum_of_local_sections
+ exists_contMDiffOn_section_forall_mem_convex_of_local
+ exists_smooth_section_forall_mem_convex_of_local
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
@michaellee94 Thanks for the quick response. You incorporated all review suggestions well - so we could just merge the PR. More precisely, your workhorse lemma
Mathlib knows an easier version of the former (for finite sums, ContMDiff.sum_section and friends). I have proven the latter in #26671; you could certainly copy-paste this code into this PR for now. I appreciate that waiting for review for months, and then being told to generalise things again can be frustrating. If you prefer, we can also merge this PR and I'll tweak the proof in a follow-up PR. * Truth be told: I haven't thought much about whether the first statement is ever used besides in partitions of unity. I did need the second one, somewhere in #26221. @PatrickMassot What do you think? |
|
Thanks for taking another look, @grunweg. I'm inclined to request a review of this PR as is, and then if a useful lemma is shown in #26671, to further simplify Edit: Actually, why not, I'll just mark that PR as a dependency of this one and give it a try. |
|
This PR/issue depends on:
|
|
Did you have any luck with the generalisation, @michaellee94? No problem if not, but since the end of the week is approaching, it would be helpful to know the current status. |
|
@michaellee94 How are things going? I just gave this a go, #27349 is how I'd prove that a locally finite sum of C^n sections is C^n. (Of course, I'm happy to compare with your solution - there may surely be ways to optimise mine.) |
|
Would you like to try and golf this PR accordingly --- or do you prefer merging this PR first, and I'll create a follow-up to golf the proof? Either way is fine with me. |
…prover-community#27349) This can be used to golf leanprover-community#26875 (and is nice API anyway). As such, it is necessary to prove the existence of a Riemannian metric (hence of a Levi-Civita connection). One could say it's on the path towards the Levi-Civita connection.
…prover-community#27349) This can be used to golf leanprover-community#26875 (and is nice API anyway). As such, it is necessary to prove the existence of a Riemannian metric (hence of a Levi-Civita connection). One could say it's on the path towards the Levi-Civita connection.
grunweg
left a comment
There was a problem hiding this comment.
I just took a look at golfing your result using the lemmas about locally finite sums of sections: there's still one more missing lemma. At this point, I think we should simply land this PR (and I can golf this in a follow-up PR).
I'd like to apply one last tweak (which is using TotalSpace.mk' instead of TotalSpace.mk and a type ascription), then this is good to go. Thanks for your work creating this (golfing some code is easier than proving it the first time!) and your patience with the review process!
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
bors d=@grunweg |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
…prover-community#27349) This can be used to golf leanprover-community#26875 (and is nice API anyway). As such, it is necessary to prove the existence of a Riemannian metric (hence of a Levi-Civita connection). One could say it's on the path towards the Levi-Civita connection.
|
Two weeks have passed, and I am excited to get this in. Let me apply my review suggestions myself, so this doesn't fail on the last step towards getting merged. Thanks a lot, @michaellee94, for making this PR in the first place (and sorry if this is stepping on your toes)! |
|
bors merge |
…on for nontrivial bundles (#26875) Add existence of global C^n smooth section for nontrivial bundles Co-authored-by: grunweg <rothgang@math.uni-bonn.de>
|
Pull request successfully merged into master. Build succeeded: |
…on for nontrivial bundles (leanprover-community#26875) Add existence of global C^n smooth section for nontrivial bundles Co-authored-by: grunweg <rothgang@math.uni-bonn.de>
…nity#28046) From the path towards the existence of Riemannian metrics, i.e. towards the Levi-Civita connection.
…on for nontrivial bundles (leanprover-community#26875) Add existence of global C^n smooth section for nontrivial bundles Co-authored-by: grunweg <rothgang@math.uni-bonn.de>
…nity#28046) From the path towards the existence of Riemannian metrics, i.e. towards the Levi-Civita connection.
…nity#28046) From the path towards the existence of Riemannian metrics, i.e. towards the Levi-Civita connection.
Add existence of global C^n smooth section for nontrivial bundles
contMDiff_section_of_tsupport#26671