Lax Lean Archive

Formal power series

Lax619925.Series · concepts/Lax619925/Series.lean · lax-619925

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

    Definition

    Formal power series over an alphabet αα are functions from words ListαList α to the rationals. They carry the pointwise vector-space structure, the left and right derivatives (the series analogues of language quotients), the reversal, the support, and the Parikh image. A series is commutative when it is constant on words with the same Parikh image. This module records the basic definitions of §2 of the paper together with the elementary facts about derivatives and reversal that the later sections use.

    Concept map
    1 concept; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 LeftRightDerivativesCommute proven

    2 ReversalInvolution proven

    3 ReversalSwapsDerivatives proven

    In the paper

    • page 8 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Real.Basic
    2import Mathlib.Data.List.Basic
    3import Mathlib.Data.Finite.Defs
    4import Mathlib.Data.Multiset.Basic
    5
    6/-!
    7---
    8title: Formal power series
    9type: definition
    10---
    11Formal power series over an alphabet `α` are functions from words `List α` to
    12the rationals. They carry the pointwise vector-space structure, the left and
    13right derivatives (the series analogues of language quotients), the reversal,
    14the support, and the Parikh image. A series is *commutative* when it is
    15constant on words with the same Parikh image. This module records the basic
    16definitions of §2 of the paper together with the elementary facts about
    17derivatives and reversal that the later sections use.
    18-/
    19
    20namespace Lax619925.Series
    21
    22-- the type and the module carrying it have the same name on purpose
    23set_option linter.dupNamespace false in
    24/-- A formal power series over the alphabet `α`: a function from words to `ℚ`. -/
    25abbrev Series (α : Type*) := List α → ℚ
    26
    27/-- The left derivative with respect to the letter `a`:
    28 `(leftDeriv a f) w = f (a :: w)`, i.e. the coefficient of `a · w` in `f`. -/
    29def leftDeriv (α : Type*) (a : α) (f : Series α) : Series α := fun w => f (a :: w)
    30
    31/-- The right derivative with respect to the letter `a`:
    32 `(rightDeriv a f) w = f (w ++ [a])`, i.e. the coefficient of `w · a` in `f`. -/
    33def rightDeriv (α : Type*) (a : α) (f : Series α) : Series α := fun w => f (w ++ [a])
    34
    35/-- The left derivative with respect to a word `w`, extended homomorphically:
    36 `(leftDerivWord w f) v = f (w ++ v)`. This agrees with the paper's recursive
    37 definition `δ^L_ε f = f` and `δ^L_{a·w} f = δ^L_w (δ^L_a f)`. -/
    38def leftDerivWord (α : Type*) (w : List α) (f : Series α) : Series α := fun v => f (w ++ v)
    39
    40/-- The right derivative with respect to a word `w`, extended homomorphically:
    41 `(rightDerivWord w f) v = f (v ++ w.reverse)`. This agrees with the paper's
    42 recursive definition `δ^R_ε f = f` and `δ^R_{w·a} f = δ^R_a (δ^R_w f)`, which
    43 appends the letters of `w` in reversed order. -/
    44def rightDerivWord (α : Type*) (w : List α) (f : Series α) : Series α := fun v => f (v ++ w.reverse)
    45
    46/-- The reversal of a series: `(reversal f) w = f (w.reverse)`. -/
    47def reversal (α : Type*) (f : Series α) : Series α := fun w => f w.reverse
    48
    49/-- The support of a series: the set of words on which it is nonzero. -/
    50def support (α : Type*) (f : Series α) : Set (List α) := {w | f w ≠ 0}
    51
    52/-- A series is a *polynomial* if its support is finite. -/
    53def IsPolynomial (α : Type*) (f : Series α) : Prop := (support α f).Finite
    54
    55/-- The Parikh image (commutative image) of a word: the function counting, for each
    56 letter, its number of occurrences in the word. The paper indexes this vector by a
    57 fixed ordering of the alphabet; the function form is equivalent and needs no order.
    58 Counting occurrences requires decidable equality on the alphabet. -/
    59def parikh (α : Type*) [DecidableEq α] (w : List α) : α → ℕ := fun a => w.count a
    60
    61/-- Two words are *commutatively equivalent* if they have the same multiset of letters,
    62 i.e. one is obtained from the other by permuting the positions of the letters.
    63 (Equivalently, when the alphabet has decidable equality, they have the same Parikh
    64 image.) -/
    65def CommutativelyEquivalent (α : Type*) (u v : List α) : Prop :=
    66 Multiset.ofList u = Multiset.ofList v
    67
    68/-- A series is *commutative* (échangeable) if it takes the same value on all
    69 commutatively equivalent words. -/
    70def IsCommutative (α : Type*) (f : Series α) : Prop :=
    71 ∀ u v, CommutativelyEquivalent α u v → f u = f v
    72
    73/-- Left and right derivatives commute: for all letters `a, b`,
    74 `leftDeriv a ∘ rightDeriv b = rightDeriv b ∘ leftDeriv a`.
    75 (Paper, §2, lemma `leftRightComm`.) Both sides send a series `f` to the series
    76 `w ↦ f (a :: w ++ [b])`. -/
    77axiom LeftRightDerivativesCommute (α : Type*) (a b : α) :
    78 leftDeriv α a ∘ rightDeriv α b = rightDeriv α b ∘ leftDeriv α a
    79
    80/-- Reversal is an involution on series. -/
    81axiom ReversalInvolution (α : Type*) (f : Series α) : reversal α (reversal α f) = f
    82
    83/-- Reversal interchanges left and right derivatives:
    84 `reversal (leftDeriv a f) = rightDeriv a (reversal f)`.
    85 Composing with the involution gives the paper's double-reversal identity
    86 `rightDeriv a f = reversal (leftDeriv a (reversal f))` used in §4. -/
    87axiom ReversalSwapsDerivatives (α : Type*) (a : α) (f : Series α) :
    88 reversal α (leftDeriv α a f) = rightDeriv α a (reversal α f)
    89
    90end Lax619925.Series
    91
    Show ProofShow ProofShow Proof
    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…