Lax Lean Archive

Formal changes of coordinates

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

definition

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

    Definition

    A formal change of coordinates is a real algebra automorphism of R[[q1,…,qd]]\mathbb R[[q_1,\ldots,q_d]] fixing the origin, continuous in both directions for the formal topology. Its coordinate images and their inverse images have zero constant term. Dimension zero is allowed.

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

    Lean source view on GitHub

    1import Lax825748.FormalSeries
    2
    3/-!
    4---
    5title: Formal changes of coordinates
    6type: definition
    7---
    8A formal change of coordinates is a real algebra automorphism of
    9R[[q1,…,qd]]\mathbb R[[q_1,\ldots,q_d]] fixing the origin, continuous in both
    10directions for the formal topology. Its coordinate images and their inverse
    11images have zero constant term. Dimension zero is allowed.
    12-/
    13
    14noncomputable section
    15
    16namespace Lax825748.CoordinateChange
    17
    18open FormalSeries
    19
    20structure FormalChange (d : ℕ) where
    21 toAlgEquiv : StateSeries d ≃ₐ[ℝ] StateSeries d
    22 continuous_toFun : FormallyContinuous toAlgEquiv
    23 continuous_invFun : FormallyContinuous toAlgEquiv.symm
    24 origin : ∀ i, MvPowerSeries.constantCoeff (toAlgEquiv (MvPowerSeries.X i)) = 0
    25 inverse_origin : ∀ i,
    26 MvPowerSeries.constantCoeff (toAlgEquiv.symm (MvPowerSeries.X i)) = 0
    27
    28end Lax825748.CoordinateChange
    29
    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…