Lax Lean Archive

Convergent coordinates on an annihilator

Lax825748.AnalyticCoordinates · concepts/Lax825748/AnalyticCoordinates.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

    Let T1,…,TdT_1,\ldots,T_d be normalized, zero-constant coordinates on J⊥J^\perp as in Proposition 1, each satisfying (C). Every element of J⊥J^\perp satisfying (C) is a convergent series in the TiT_i.

    Indeed, the TiT_i are convergent series in PBW coordinates and have identity linear part. Their inverse change of coordinates is convergent by the analytic inverse function theorem.

    Concept map
    15 concepts; 3 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.PBWConvergence
    2import Lax825748.AnalyticCalculus
    3import Lax825748.AnalyticChanges
    4
    5/-!
    6---
    7title: Convergent coordinates on an annihilator
    8type: theorem
    9---
    10Let T1,…,TdT_1,\ldots,T_d be normalized, zero-constant coordinates on J⊥J^\perp
    11as in Proposition 1, each satisfying (C). Every element of J⊥J^\perp
    12satisfying (C) is a convergent series in the TiT_i.
    13
    14Indeed, the TiT_i are convergent series in PBW coordinates and have
    15identity linear part. Their inverse change of coordinates is convergent
    16by the analytic inverse function theorem.
    17-/
    18
    19noncomputable section
    20
    21namespace Lax825748.AnalyticCoordinates
    22
    23open Lax825748.Series Lax825748.LieRank Lax825748.Annihilator
    24open Lax825748.FormalSeries ConvergentSeries
    25
    26axiom expansion_converges {X : Type} {d : ℕ}
    27 (K : LieSubalgebraOfPolynomials X) (P : Fin d → LiePolynomial X)
    28 (hP : IsComplement K P) (T : Fin d → NCSeries X)
    29 (hT : IsCoordinateFamily K P T)
    30 (hCT : ∀ i, ConvergenceHypothesis.Holds (T i))
    31 (U : NCSeries X) (hU : InAnnihilator K U)
    32 (hCU : ConvergenceHypothesis.Holds U) :
    33 ∃ f : StateSeries d, Convergent f ∧ substituteShuffle T f = U
    34
    35end Lax825748.AnalyticCoordinates
    36
    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…