Documentation

Mathlib.Geometry.Manifold.AnalyticManifold

Analytic manifolds (possibly with boundary or corners) #

An analytic manifold is a manifold modelled on a normed vector space, or a subset like a half-space (to get manifolds with boundaries) for which changes of coordinates are analytic in the interior and smooth everywhere (including at the boundary). The definition mirrors SmoothManifoldWithCorners, but using an analyticGroupoid in place of contDiffGroupoid. All analytic manifolds are smooth manifolds.

For now we define only analyticGroupoid; an upcoming commit will add AnalyticManifold (see https://github.com/leanprover-community/mathlib4/pull/10853).

analyticGroupoid #

f ∈ PartialHomeomorph H H is in analyticGroupoid I if f and f.symm are smooth everywhere, analytic on the interior, and map the interior to itself. This allows us to define AnalyticManifold including in cases with boundary.

source
def analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) :
StructureGroupoid H

Given a model with corners (E, H), we define the groupoid of analytic transformations of H as the maps that are analytic and map interior to interior when read in E through I. We also explicitly define that they are C^∞ on the whole domain, since we are only requiring analyticity on the interior of the domain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ofSet_mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H} (hs : IsOpen s) :
    PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I

    An identity partial homeomorphism belongs to the analytic groupoid.

    source
    theorem symm_trans_mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] (e : PartialHomeomorph M H) :
    e.symm.trans e ∈ analyticGroupoid I

    The composition of a partial homeomorphism from H to M and its inverse belongs to the analytic groupoid.

    source
    instance instClosedUnderRestrictionAnalyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) :
    ClosedUnderRestriction (analyticGroupoid I)

    The analytic groupoid is closed under restriction.

    Equations
    • ⋯ = ⋯
    source
    theorem mem_analyticGroupoid_of_boundaryless {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [CompleteSpace E] [I.Boundaryless] (e : PartialHomeomorph H H) :
    e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I '' e.source) ∧ AnalyticOn 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I '' e.target)

    The analytic groupoid on a boundaryless charted space modeled on a complete vector space consists of the partial homeomorphisms which are analytic and have analytic inverse.