feat: extend smoothness category of manifolds with corners to include analytic manifolds

[sgouezel]

Now that ContDiff includes smoothness exponents up to analytic functions, we can do the same for manifolds. The PR renames SmoothManifoldWithCorners to ContMDiffManifoldWithCorners, and includes an additional smoothness exponent (ranging from 0 to infinity and omega).

The file SmoothManifoldWithCorners itself is not renamed, to avoid confusing git, and will be renamed in a follow-up PR.

The current version of the PR also allows an additional smoothness exponent in the algebraic classes like ContMDiffMul or LieGroup. I wonder if we should not just settle on omega for these, as all the interesting examples are analytic (and there is a theorem saying that any real Lie group has a compatible analytic structure).

I also wonder if we should rename ContMDiffManifoldWithCorners to something much shorter like IsManifold.

I still have to add deprecations. Also, I've deleted the file AnalyticManifold now that it's superseded by the general notion. Should I instead keep it and deprecate everything in there? Or move it to the Deprecated folder?

---

• depends on: [Merged by Bors] - feat: unique differentiability of preimages under projection doesn't need the bundle to be smooth #19682

[github-actions]

PR summary e0b6ad01ed

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.AnalyticManifold	1766	0	-1766 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.AnalyticManifold	-1766

---

Declarations diff

+ Bundle.Prod.contMDiffVectorBundle
+ Bundle.TotalSpace.isManifold
+ Bundle.Trivial.contMDiffVectorBundle
+ ContMDiffAdd
+ ContMDiffAddMonoidMorphism
+ ContMDiffAt.of_succ(h
+ ContMDiffFunction.evalAt
+ ContMDiffInv₀
+ ContMDiffMonoidMorphism
+ ContMDiffMul
+ ContMDiffRing
+ ContMDiffVectorBundle
+ ContMDiffVectorBundle.continuousLinearMap
+ ContMDiffVectorBundle.of_le
+ ContMDiffVectorBundle.pullback
+ EuclideanSpace.instIsManifoldSphere
+ IsManifold
+ IsManifold.locallyRingedSpace
+ IsManifold.mk'
+ OpenEmbedding.singleton_IsManifold
+ PartialHomeomorph.isManifold_singleton
+ PointedContMDiffMap
+ StructureGroupoid.maximalAtlas_mono
+ TangentBundle.contMDiffVectorBundle
+ Topology.IsOpenEmbedding.isManifold_singleton
+ _root_.ENat.LEInfty
+ contDiffWithinAt_localInvariantProp_of_le
+ contMDiffAt_infty
+ contMDiffOn_infty
+ contMDiffOn_zero_iff
+ contMDiffVectorBundle
+ contMDiffWithinAt_infty
+ contMDiff_infty
+ contMDiff_zero_iff
+ hasContinuousInv₀_of_hasContMDiffInv₀
+ instContMDiffVectorBundle
+ instIsManifoldIcc
+ instIsManifoldTransDiffeomorph
+ instance (n : ℕ) : LEInfty (n : WithTop ℕ∞) := ⟨mod_cast le_top⟩
+ instance (n : ℕ) [n.AtLeastTwo] : LEInfty (no_index (OfNat.ofNat n) : WithTop ℕ∞)
+ instance (priority := 100) fieldSmoothRing
+ instance : ContMDiffVectorBundle 0 F E IB := by
+ instance : ContinuousMapClass (ContMDiffMonoidMorphism I I' n G G') G G'
+ instance : FunLike (ContMDiffMonoidMorphism I I' n G G') G G'
+ instance : Inhabited (ContMDiffMonoidMorphism I I' n G G')
+ instance : IsManifold (𝓡 1) ω Circle
+ instance : IsManifold I 0 M := by
+ instance : IsManifold I n s
+ instance : IsManifold 𝓘(ℂ) ω ℍ
+ instance : IsManifold 𝓘(𝕜, R) n Rˣ
+ instance : LEInfty (0 : WithTop ℕ∞) := inferInstanceAs (LEInfty ((0 : ℕ) : WithTop ℕ∞))
+ instance : LEInfty (1 : WithTop ℕ∞) := inferInstanceAs (LEInfty ((1 : ℕ) : WithTop ℕ∞))
+ instance : LieGroup (𝓡 1) ω Circle
+ instance : LieGroup 𝓘(𝕜, R) n Rˣ
+ instance : MonoidHomClass (ContMDiffMonoidMorphism I I' n G G') G G'
+ instance : One (ContMDiffMonoidMorphism I I' n G G')
+ instance [ContMDiffVectorBundle 2 F E IB] : ContMDiffVectorBundle 1 F E IB
+ instance [IsManifold I 2 M] :
+ instance [IsManifold I ω M] :
+ instance [h : IsManifold I 2 M] :
+ instance [h : IsManifold I ∞ M] :
+ instance {a : WithTop ℕ∞} [ContMDiffVectorBundle ω F E IB] : ContMDiffVectorBundle a F E IB
+ instance {a : WithTop ℕ∞} [ContMDiffVectorBundle ∞ F E IB] [h : ENat.LEInfty a] :
+ instance {a : WithTop ℕ∞} [IsManifold I ω M] :
+ instance {a : WithTop ℕ∞} [IsManifold I ∞ M] [h : LEInfty a] :
+ instance {n : WithTop ℕ∞} : IsManifold (𝓡∂ 1) n (Icc (0 : ℝ) 1) := by
+ instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+ instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : ContMDiffInv₀ 𝓘(𝕜) n 𝕜
+ isManifold_of_contDiffOn
+ maximalAtlas_subset_of_le
+ of_le
+-+- IsSmooth
- AnalyticManifold
- AnalyticManifold.prod
- AnalyticManifold.self
- AnalyticManifold.smoothManifoldWithCorners
- Bundle.Prod.smoothVectorBundle
- Bundle.TotalSpace.smoothManifoldWithCorners
- Bundle.Trivial.smoothVectorBundle
- ContMDiffAt.of_succ
- EuclideanSpace.instSmoothManifoldWithCornersSphere
- Icc_smoothManifoldWithCorners
- OpenEmbedding.singleton_smoothManifoldWithCorners
- PartialHomeomorph.singleton_smoothManifoldWithCorners
- PointedSmoothMap
- SmoothAdd
- SmoothAddMonoidMorphism
- SmoothFunction.evalAt
- SmoothInv₀
- SmoothManifoldWithCorners
- SmoothManifoldWithCorners.locallyRingedSpace
- SmoothManifoldWithCorners.mk'
- SmoothMonoidMorphism
- SmoothMul
- SmoothRing
- SmoothVectorBundle
- SmoothVectorBundle.continuousLinearMap
- SmoothVectorBundle.pullback
- TangentBundle.smoothVectorBundle
- Topology.IsOpenEmbedding.singleton_smoothManifoldWithCorners
- analyticGroupoid
- analyticGroupoid_prod
- analyticPregroupoid
- contMDiffAt_top
- contMDiffOn_top
- contMDiffWithinAt_top
- contMDiff_top
- hasContinuousInv₀_of_hasSmoothInv₀
- instance (priority := 100) fieldSmoothRing {𝕜 : Type*} [NontriviallyNormedField 𝕜] :
- instance : ClosedUnderRestriction (analyticGroupoid I)
- instance : ContinuousMapClass (SmoothMonoidMorphism I I' G G') G G'
- instance : FunLike (SmoothMonoidMorphism I I' G G') G G'
- instance : Inhabited (SmoothMonoidMorphism I I' G G')
- instance : LieGroup (𝓡 1) Circle
- instance : LieGroup 𝓘(𝕜, R) Rˣ
- instance : MonoidHomClass (SmoothMonoidMorphism I I' G G') G G'
- instance : One (SmoothMonoidMorphism I I' G G')
- instance : SmoothManifoldWithCorners (𝓡 1) Circle
- instance : SmoothManifoldWithCorners (𝓡∂ 1) (Icc (0 : ℝ) 1) := by infer_instance
- instance : SmoothManifoldWithCorners I s
- instance : SmoothManifoldWithCorners 𝓘(ℂ) ℍ
- instance : SmoothManifoldWithCorners 𝓘(𝕜, R) Rˣ
- instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] : SmoothInv₀ 𝓘(𝕜) 𝕜
- instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H] {E : Type*}
- mem_analyticGroupoid
- mem_analyticGroupoid_of_boundaryless
- ofSet_mem_analyticGroupoid
- smoothManifoldWithCorners_of_contDiffOn
- smoothManifoldWithCorners_transDiffeomorph
- symm_trans_mem_analyticGroupoid
-- smoothVectorBundle

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.

---

Decrease in tech debt: (relative, absolute) = (1.13, 0.01)

Current number	Change	Type
222	-1	bare open (scoped) Classical
4878	-4	exceptions for the docPrime linter

Current commit e0b6ad01ed
Reference commit 41cbc10ab1

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]

About naming: how about IsManifoldWithCorners? I agree ContDiff is superfluous, given the exponent as an explicit parameter.

[grunweg]

This change means the following paragraph is also obsolete --- right? Can you take a pass over the module doc-string to ensure the implementation notes are up to date?

We concentrate on C^∞ manifolds: all the definitions work equally well for C^n manifolds, but later on it is a pain to carry all over the smoothness parameter, especially when one wants to deal with C^k functions as there would be additional conditions k ≤ n everywhere. Since one deals almost all the time with C^∞ (or analytic) manifolds, this seems to be a reasonable choice that one could revisit later if needed. C^k manifolds are still available, but they should be called using [HasGroupoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/ChartedSpace.html#HasGroupoid) M (contDiffGroupoid k I) where I is the model with corners.

[sgouezel]

Yes, I will need to pass over all docs to adjust it to the new setting. I'll do that once people agree on what they want in the Zulip discussion.

[grunweg]

Three small comments; I have to turn to other things now.

Can you add deprecations for the old names, please? Thanks for doing this refactor!

[sgouezel]

I'll add the deprecations once everything has been sorted out in the Zulip discussion: no need to do the same work two or three times...

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: unique differentiability of preimages under projection doesn't need the bundle to be smooth #19682
  By Dependent Issues (🤖). Happy coding!

[grunweg]

I've reviewed everything once, except for

• Geometry/Manifold/Algebra/Monoid.lean
• Geometry/Manifold/Algebra/SmoothFunctions.lean
• Geometry/Manifold/AnalyticManifold.lean
• Geometry/Manifold/ContMDiff/Defs.lean
• Geometry/Manifold/SmoothManifoldWithCorners.lean

Mostly very minor comments. This PR is so cross-cutting that also doc-strings and lemma names can go stale: because you generalise things to C^n where appropriate, I think some more things should be called "contDiffThing" and not "smoothThing".
I didn't read the file changing it yet, but "smoothMaximalAtlas" is another such example.

I'm repeating myself, but let me say it again anyway: thanks for attempting this monumental feat. It's only natural that there are lots of little details that can go stale.

I've reviewed this diff "from the bottom", so if something is confusing, you may want to read the comments in opposite order.

[grunweg]

Write this on one line? Same above.

[grunweg]

These lemmas are now generalised to their appropriate context: would you like to mention this in the PR description as well? (This is a positive change!)

[grunweg]

Please double-check this module doc-string as well: there are still lots of mentions of "smooth vector bundles" or "smooth manifolds". In fact, this file proves them for $C^n$ (and analytic) bundles/manifolds now - let's show this to users of this file!

[grunweg]

Should smoothCoordinateChange (and SmoothVectorPrebundle) also be renamed?

[grunweg]

Ah, they already were: please update the doc-string on (current) line 642 then.

[grunweg]

Please update this comment; also the one below.

[grunweg]

(And perhaps search for similar examples in mathlib: I only looked at the diff so far, not searched mathlib if there were further patterns.)

[grunweg]

These are annoying, but perhaps that's the price of such a major refactoring. It need not block in this, in any case.

[grunweg]

Please update this doc-string: "for any n" is now false. (I haven't checked if other doc-strings in this file are also stale now.)

[grunweg]

Happy to approve this "immediately" if you extract it into a separate PR. (If you think the book-keeping is worth it.)
The same applies to other such clean-ups, I've noted at least one more in my review.

[grunweg]

Should this name also be updated? It also includes C^n, after all.

[grunweg]

Should this instance name be updated also?