Lax Lean Archive

Analytic differential representations

Lax825748.AnalyticRepresentations · concepts/Lax825748/AnalyticRepresentations.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 differential representation is analytic if its output series and every coefficient of each of its vector fields converge near the origin. Its generated coefficient at a word ww is the constant term of hμwh\mu w, with the vector fields acting on the right in the order of the letters. A series is analytically produced if such a representation exists in some finite dimension, including dimension zero.

    Convergence of the vector fields is required explicitly. It is used in the proof and in the interpretation by analytic systems, although omitted from the printed Definition 1.

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

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.ConvergentSeries
    2import Lax825748.DifferentialRepresentation
    3
    4/-!
    5---
    6title: Analytic differential representations
    7type: definition
    8---
    9A differential representation is analytic if its output series and every
    10coefficient of each of its vector fields converge near the origin.
    11Its generated coefficient at a word ww is the constant term of hμwh\mu w,
    12with the vector fields acting on the right in the order of the letters.
    13A series is analytically produced if such a representation exists in some
    14finite dimension, including dimension zero.
    15
    16Convergence of the vector fields is required explicitly. It is used in
    17the proof and in the interpretation by analytic systems, although omitted
    18from the printed Definition 1.
    19-/
    20
    21noncomputable section
    22
    23namespace Lax825748.AnalyticRepresentations
    24
    25open Lax825748.Series Lax825748.DifferentialRepresentation ConvergentSeries
    26
    27def IsAnalytic {X : Type} {d : ℕ} (R : Representation X d) : Prop :=
    28 Convergent R.output ∧ ∀ x i, Convergent (R.fields x i)
    29
    30def AnalyticallyProduced {X : Type} (g : NCSeries X) : Prop :=
    31 ∃ d, ∃ R : Representation X d, IsAnalytic R ∧ Represents R g
    32
    33end Lax825748.AnalyticRepresentations
    34
    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…