Lax Lean Archive

Analytic equivalence of minimal realizations

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

    Two analytic differential representations of a series of Lie rank dd, both of dimension dd, are related by an analytic change of coordinates fixing the origin. This change sends the first output to the second and intertwines the action of every word on every state series. Its inverse is also convergent and formally continuous.

    Concept map
    28 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.Minimality
    2import Lax825748.AnalyticChanges
    3import Lax825748.FormalUniqueness
    4
    5/-!
    6---
    7title: Analytic equivalence of minimal realizations
    8type: theorem
    9---
    10Two analytic differential representations of a series of Lie rank dd,
    11both of dimension dd, are related by an analytic change of coordinates
    12fixing the origin. This change sends the first output to the second and
    13intertwines the action of every word on every state series.
    14Its inverse is also convergent and formally continuous.
    15-/
    16
    17noncomputable section
    18
    19namespace Lax825748.Uniqueness
    20
    21open Lax825748.Series Lax825748.LieRank Lax825748.FormalSeries
    22open Lax825748.DifferentialRepresentation AnalyticRepresentations AnalyticChanges
    23
    24axiom minimal_realizations_equivalent {X : Type} [Finite X] {d : ℕ}
    25 (g : NCSeries X) (hr : HasLieRank g d)
    26 (R R' : Representation X d) (hR : Represents R g) (hR' : Represents R' g)
    27 (ha : IsAnalytic R) (ha' : IsAnalytic R') :
    28 ∃ φ : AnalyticChange d,
    29 φ.toAlgEquiv R.output = R'.output ∧
    30 ∀ (k : StateSeries d) (w : Word X),
    31 φ.toAlgEquiv (act R k w) = act R' (φ.toAlgEquiv k) w
    32
    33end Lax825748.Uniqueness
    34
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…