Lax Lean Archive

Noncommutative series and polynomial residuals

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

    For an alphabet XX, a series is a function X∗→RX^*\to\mathbb R and a polynomial is a finite real linear combination of words. Polynomial multiplication is concatenation. The pairing is (S,P)=∑wPwSw(S,P)=\sum_w P_w S_w.

    The two residuals are (S∘P,w)=(S,Pw)(S\circ P,w)=(S,Pw) and (P∘S,w)=(S,wP)(P\circ S,w)=(S,wP). The empty word is the monoid identity. Agreement below degree NN means equality at every word of length less than NN.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.MonoidAlgebra.Basic
    2import Mathlib.Algebra.FreeMonoid.Basic
    3import Mathlib.Data.Real.Basic
    4
    5/-!
    6---
    7title: Noncommutative series and polynomial residuals
    8type: definition
    9---
    10For an alphabet XX, a series is a function X∗→RX^*\to\mathbb R and a polynomial
    11is a finite real linear combination of words. Polynomial multiplication is
    12concatenation. The pairing is (S,P)=∑wPwSw(S,P)=\sum_w P_w S_w.
    13
    14The two residuals are (S∘P,w)=(S,Pw)(S\circ P,w)=(S,Pw) and
    15(P∘S,w)=(S,wP)(P\circ S,w)=(S,wP). The empty word is the monoid identity.
    16Agreement below degree NN means equality at every word of length less than NN.
    17-/
    18
    19noncomputable section
    20
    21namespace Lax825748.Series
    22
    23abbrev Word (X : Type) := FreeMonoid X
    24abbrev NCSeries (X : Type) := Word X → ℝ
    25abbrev NCPolynomial (X : Type) := MonoidAlgebra ℝ (Word X)
    26
    27noncomputable def pairing {X : Type} (S : NCSeries X) (P : NCPolynomial X) : ℝ :=
    28 P.coeff.sum fun w a => a * S w
    29
    30noncomputable def wordPolynomial {X : Type} (w : Word X) : NCPolynomial X :=
    31 MonoidAlgebra.single w 1
    32
    33noncomputable def letter {X : Type} (x : X) : NCPolynomial X :=
    34 wordPolynomial (FreeMonoid.of x)
    35
    36noncomputable def rightResidual {X : Type} (S : NCSeries X)
    37 (P : NCPolynomial X) : NCSeries X :=
    38 fun w => pairing S (P * wordPolynomial w)
    39
    40noncomputable def leftResidual {X : Type} (P : NCPolynomial X)
    41 (S : NCSeries X) : NCSeries X :=
    42 fun w => pairing S (wordPolynomial w * P)
    43
    44noncomputable def constantSeries {X : Type} (a : ℝ) : NCSeries X := by
    45 classical
    46 exact fun w => if w = 1 then a else 0
    47
    48def AgreeBelow {X : Type} (N : ℕ) (S T : NCSeries X) : Prop :=
    49 ∀ w, w.toList.length < N → S w = T w
    50
    51def FormallyContinuous {X Y : Type} (F : NCSeries X → NCSeries Y) : Prop :=
    52 ∀ N, ∃ M, ∀ S T, AgreeBelow M S T → AgreeBelow N (F S) (F T)
    53
    54end Lax825748.Series
    55
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…