Lax Lean Archive

Analytic changes of coordinates

Lax825748.AnalyticChanges · concepts/Lax825748/AnalyticChanges.lean · lax-825748

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    An analytic change of coordinates is a formally continuous real algebra automorphism fixing the origin whose coordinate images, in both directions, are convergent power series.

    The analytic inverse function theorem implies that a formal change of coordinates with convergent coordinate images has convergent inverse images. This is the implicit function theorem used in part b) of the paper.

    Concept map
    6 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.ConvergentSeries
    2import Lax825748.CoordinateChange
    3
    4/-!
    5---
    6title: Analytic changes of coordinates
    7type: theorem
    8---
    9An analytic change of coordinates is a formally continuous real algebra
    10automorphism fixing the origin whose coordinate images, in both directions,
    11are convergent power series.
    12
    13The analytic inverse function theorem implies that a formal change of
    14coordinates with convergent coordinate images has convergent inverse images.
    15This is the implicit function theorem used in part b) of the paper.
    16-/
    17
    18noncomputable section
    19
    20namespace Lax825748.AnalyticChanges
    21
    22open Lax825748.FormalSeries Lax825748.CoordinateChange ConvergentSeries
    23
    24structure AnalyticChange (d : ℕ) extends FormalChange d where
    25 convergent_toFun : ∀ i, Convergent (toAlgEquiv (MvPowerSeries.X i))
    26 convergent_invFun : ∀ i, Convergent (toAlgEquiv.symm (MvPowerSeries.X i))
    27
    28axiom inverse_convergent {d : ℕ} (φ : FormalChange d)
    29 (hφ : ∀ i, Convergent (φ.toAlgEquiv (MvPowerSeries.X i))) :
    30 ∀ i, Convergent (φ.toAlgEquiv.symm (MvPowerSeries.X i))
    31
    32end Lax825748.AnalyticChanges
    33
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…