Lax Lean Archive

Local analytic realization of generating series

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

    For a finite alphabet, a real noncommutative series admits an analytic differential representation if and only if it has finite Lie rank and satisfies (C). If its Lie rank is dd, a representation of dimension exactly dd exists.

    The realization is obtained in the normalized residual coordinates Ti=g∘Qi−(g,Qi)T_i=g\circ Q_i-(g,Q_i). Convergence of the output and of the vector-field coefficients follows from their convergent coordinate expansions.

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 characterization proven

    2 existence proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.AnalyticRepresentations
    2import Lax825748.NecessaryConvergence
    3import Lax825748.ResidualConvergence
    4import Lax825748.AnalyticCoordinates
    5import Lax825748.FormalMinimality
    6
    7/-!
    8---
    9title: Local analytic realization of generating series
    10type: theorem
    11---
    12For a finite alphabet, a real noncommutative series admits an analytic
    13differential representation if and only if it has finite Lie rank and
    14satisfies (C). If its Lie rank is dd, a representation of dimension
    15exactly dd exists.
    16
    17The realization is obtained in the normalized residual coordinates
    18Ti=g∘Qi−(g,Qi)T_i=g\circ Q_i-(g,Q_i). Convergence of the output and of the vector-field
    19coefficients follows from their convergent coordinate expansions.
    20-/
    21
    22noncomputable section
    23
    24namespace Lax825748.Realization
    25
    26open Lax825748.Series Lax825748.LieRank Lax825748.DifferentialRepresentation
    27open AnalyticRepresentations
    28
    29axiom existence {X : Type} [Finite X] (g : NCSeries X) (d : ℕ)
    30 (hr : HasLieRank g d) (hC : ConvergenceHypothesis.Holds g) :
    31 ∃ R : Representation X d, IsAnalytic R ∧ Represents R g
    32
    33axiom characterization {X : Type} [Finite X] (g : NCSeries X) :
    34 AnalyticallyProduced g ↔ FiniteLieRank g ∧ ConvergenceHypothesis.Holds g
    35
    36end Lax825748.Realization
    37
    Show ProofShow 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…