Commit 2025-01-09 15:36 3dff5d2c

feat: extend smoothness category of manifolds with corners to include analytic manifolds (#19696) Now that ContDiff includes smoothness exponents up to analytic functions, we can do the same for manifolds. The PR renames SmoothManifoldWithCorners to IsManifold, and includes an additional smoothness exponent (ranging from 0 to infinity and omega). The docstring of IsManifold emphasizes that this allows (but does not mandate) corners or boundaries. 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. For all of these, we add a bunch of instances to deduce low smoothness from high smoothness versions (for example, LieGroup I 2 G is found by typeclass inference from LieGroup I ∞ G). This change makes it possible to do things with the correct assumptions. For instance, the tangent bundle is a fiber bundle assuming only that the manifold is C^1 (but we have instances saying that it is C^∞ if the manifold is C^∞, analytic if the manifold is analytic). Normally, I should have properly deprecated everything but instances. TODO in follow-up PRs:

• rename SmoothManifoldWithCorners.lean to IsManifold.lean
• deprecate the whole file Manifold.Analytic.lean