Lax Lean Archive

Convergence of PBW coordinate expansions

Lax825748.PBWConvergence · concepts/Lax825748/PBWConvergence.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 P1,…,PdP_1,\ldots,P_d be a basis modulo a Lie subalgebra L0L_0, and let S1,…,SdS_1,\ldots,S_d be the associated PBW coordinates of J⊥J^\perp, where J=R⟨X⟩L0J=\mathbb R\langle X\rangle L_0. If T∈J⊥T\in J^\perp satisfies (C), its coordinate expansion is convergent. The coefficient of SIS^I is (T,PI)/I!(T,P^I)/I!, so (C) is precisely the required geometric bound for this expansion.

    Concept map
    11 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.ConvergenceHypothesis
    3import Lax825748.Annihilator
    4
    5/-!
    6---
    7title: Convergence of PBW coordinate expansions
    8type: theorem
    9---
    10Let P1,…,PdP_1,\ldots,P_d be a basis modulo a Lie subalgebra L0L_0, and let
    11S1,…,SdS_1,\ldots,S_d be the associated PBW coordinates of
    12J⊥J^\perp, where J=R⟨X⟩L0J=\mathbb R\langle X\rangle L_0.
    13If T∈J⊥T\in J^\perp satisfies (C), its coordinate expansion is convergent.
    14The coefficient of SIS^I is (T,PI)/I!(T,P^I)/I!, so (C) is precisely the
    15required geometric bound for this expansion.
    16-/
    17
    18noncomputable section
    19
    20namespace Lax825748.PBWConvergence
    21
    22open Lax825748.Series Lax825748.LieRank Lax825748.Annihilator
    23open Lax825748.FormalSeries ConvergentSeries
    24
    25axiom expansion_converges {X : Type} {d : ℕ}
    26 (K : LieSubalgebraOfPolynomials X) (P : Fin d → LiePolynomial X)
    27 (hP : IsComplement K P) (S : Fin d → NCSeries X)
    28 (hS : IsCoordinateFamily K P S) (hPBW : IsPBWCoordinateFamily P S)
    29 (T : NCSeries X) (hT : InAnnihilator K T)
    30 (hC : ConvergenceHypothesis.Holds T) :
    31 ∃ f : StateSeries d, Convergent f ∧ substituteShuffle S f = T
    32
    33end Lax825748.PBWConvergence
    34
    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…