[Merged by Bors] - feat: Define AnalyticManifold as a charted space compatible with analyticGroupoid#10853
[Merged by Bors] - feat: Define AnalyticManifold as a charted space compatible with analyticGroupoid#10853
AnalyticManifold as a charted space compatible with analyticGroupoid#10853Conversation
|
To foreshadow, the next thing I need to define is manifold-analytic maps. Currently I have these defined at https://github.com/girving/ray/blob/be98efd5d2fb6dad741c905262a93bb9aa6eaf49/Ray/AnalyticManifold/AnalyticManifold.lean#L248 only in the boundaryless case, which means analytic in charts. We’ll need to choose how to extend this to the boundaries. The natural thing following There’s some awkwardness in that basic theory if we require only smoothness at boundary points won’t look like normal analytic functions. In particular, an analytic function at a point is locally analytic, but this wouldn’t be true if I’ll note that the “smooth at boundary” setup makes analyticGroupoid nontrivially more complex, and I’m not sure what it buys us: I haven’t seen that definition before, and currently analyticGroupoid is unused in mathlib. |
|
I have to say that I don't really understand why we use this definition of analytic groupoid instead of the more direct definition "analytic at every point, including the boundary". Do you understand what the more complicated definition buys us? |
|
No, I don't understand what the more complicated definition buys us. I haven't seen it elsewhere in mathematics: it's common to want "analytic inside, continuous at the boundary", but smooth I haven't seen (and I think analytic inside, continuous at the boundary is better named something else). If we want to do analytic at the boundary we need some additional definitions, though, since we don't have I'd be happy to make that change if people think it's the right thing. |
|
Here's the PR where it was added: #6386. I don't see discussion there of the smoothness part, but I may have just failed to expand the right comment thread. Cc @michaellee94. |
|
Thanks for the ping, @girving. I seem to recall having some difficulty with the pregroupoid definition when I tried to extend analyticity to the boundary (this was only my second PR, so I'm still a mathlib neophyte). If you have a working implementation, I would love to take a look. Additionally, my intention was to re-implement the existing examples of smooth manifolds (the interval, the sphere) in the analytic setting--I've changed jobs recently and haven't had the time, but I still think it would be valuable. |
|
The sphere is https://github.com/girving/ray/blob/main/Ray/AnalyticManifold/RiemannSphere.lean, and any reasonable subset of an So from your perspective, if I can make |
Very nice!
Certainly, at least for me. |
|
I've updated the definition to require analyticity including on the boundary. There are two main warts:
|
PR summary f2d9f2b4c0
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.AnalyticManifold | 1549 | 1551 | +2 (+0.13%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.AnalyticManifold |
2 |
Declarations diff
+ AnalyticManifold
+ AnalyticManifold.prod
+ AnalyticManifold.self
+ AnalyticManifold.smoothManifoldWithCorners
+ analyticGroupoid_prod
+ analyticPregroupoid
+ mem_analyticGroupoid
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.
|
@sgouezel Wow, thank you for resurrecting this! Let me know if I can help, though it seems like it’s passing now. |
There was a problem hiding this comment.
Thanks for your PR; I'm still excited to see it! I wonder how this could get merged best.
For instance: this PR is quite large; I think splitting into several parts could speed up the review. The zero radius and constFormalMultilinearSeries_zero] look good; if you make a PR for those, I'd approve that quickly. Perhaps, the Analytic/Within file could also be a separate PR.
Edited to add: I realised that simply moving the definition of AnalyticGroupoid could be another quick PR.
Reviewing time is very much super-linear in the PR size, so splitting off easy pieces makes this job easier and usually faster.
This is a few isolated lemmas split out of #10853. 1. AnalyticAt.comp_of_eq 2. FormalMultilinearSeries.zero_radius 3. constFormalMultilinearSeries_zero
I'm about to rewrite the definition of `analyticGroupoid` and define `AnalyticManifold` on top of it, in #10853. @grunweg suggested splitting out the move of `analyticGroupoid` into a separate commit, so that the diff is easier. It used to be in `SmoothManifoldWithCorners.lean`, but this makes no sense as nothing downstream of that file uses `analyticGroupoid`.
|
@grunweg Sorry for the delay merging those; I missed the notification somehow. |
|
@grunweg Are you still up for reviewing this, or we find a different reviewer? |
grunweg
left a comment
There was a problem hiding this comment.
@girving I'm very very sorry for the delay. I took a detailed look now.
Your PR looks very good to me. I have a number of comments, but they are all very minor (mostly, about compressing your code slightly). Mostly, you can simply accept the github suggestions; if you prefer, I can also make these tweaks tomorrow.
I like how the proofs about the analytic groupoid became much simpler - partly because of the simpler definition, but also because you golfed the proofs! I found a few more ways to compress your code; should be really quick. (If you prefer, I can also apply these changes myself tomorrow; let me know!)
Can you update the commit message, please - and make sure to
- mention the change of definition and some words on why
- add that you prove the product of analytic manifolds to be analytic? Thanks!
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
|
Most comments addressed! I'll await replies to the last two. |
grunweg
left a comment
There was a problem hiding this comment.
Thanks for the prompt response!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
@grunweg I fixed the commit message. |
|
bors r+ |
…nalyticGroupoid` (#10853) 1. Change the definition of `analyticGroupoid` to mean analytic everywhere including on the boundary, using the recently added `AnalyticWithinAt` def. 2. Define `AnalyticManifold` as a charted space compatible with `analyticGroupoid`. In finite dimensions `AnalyticManifold` is equivalent to `SmoothManifoldWithCorners`, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.
|
Pull request successfully merged into master. Build succeeded: |
AnalyticManifold as a charted space compatible with analyticGroupoidAnalyticManifold as a charted space compatible with analyticGroupoid
…nalyticGroupoid` (#10853) 1. Change the definition of `analyticGroupoid` to mean analytic everywhere including on the boundary, using the recently added `AnalyticWithinAt` def. 2. Define `AnalyticManifold` as a charted space compatible with `analyticGroupoid`. In finite dimensions `AnalyticManifold` is equivalent to `SmoothManifoldWithCorners`, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.
…nalyticGroupoid` (#10853) 1. Change the definition of `analyticGroupoid` to mean analytic everywhere including on the boundary, using the recently added `AnalyticWithinAt` def. 2. Define `AnalyticManifold` as a charted space compatible with `analyticGroupoid`. In finite dimensions `AnalyticManifold` is equivalent to `SmoothManifoldWithCorners`, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.
…nalyticGroupoid` (#10853) 1. Change the definition of `analyticGroupoid` to mean analytic everywhere including on the boundary, using the recently added `AnalyticWithinAt` def. 2. Define `AnalyticManifold` as a charted space compatible with `analyticGroupoid`. In finite dimensions `AnalyticManifold` is equivalent to `SmoothManifoldWithCorners`, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.
analyticGroupoidto mean analytic everywhere including on the boundary, using the recently addedAnalyticWithinAtdef.AnalyticManifoldas a charted space compatible withanalyticGroupoid.In finite dimensions
AnalyticManifoldis equivalent toSmoothManifoldWithCorners, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.