Lax Lean Archive

Shuffle multiplication

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

    Definition and theorem

    The coefficient of ww in the shuffle of SS and TT is the sum of S(w∣I)T(w∣Ic)S(w|I)T(w|I^c) over subsets of the positions of ww. Repeated letters retain their multiplicities. This product is associative and commutative, with unit the series supported at the empty word. No concatenation product on series is used here.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 associative proven

    2 commutative proven

    3 unit proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.Series
    2
    3/-!
    4---
    5title: Shuffle multiplication
    6type: definition and theorem
    7---
    8The coefficient of ww in the shuffle of SS and TT is the sum of
    9S(w∣I)T(w∣Ic)S(w|I)T(w|I^c) over subsets of the positions of ww. Repeated letters retain
    10their multiplicities. This product is associative and commutative, with unit
    11the series supported at the empty word. No concatenation product on series
    12is used here.
    13-/
    14
    15noncomputable section
    16
    17namespace Lax825748.Shuffle
    18
    19open Series
    20
    21def unshuffles {X : Type} : List X → List (List X × List X)
    22 | [] => [([], [])]
    23 | x :: w => (unshuffles w).flatMap fun p =>
    24 [(x :: p.1, p.2), (p.1, x :: p.2)]
    25
    26noncomputable def shuffle {X : Type} (S T : NCSeries X) : NCSeries X :=
    27 fun w => ((unshuffles w.toList).map fun p =>
    28 S (FreeMonoid.ofList p.1) * T (FreeMonoid.ofList p.2)).sum
    29
    30noncomputable def shuffleList {X : Type} : List (NCSeries X) → NCSeries X
    31 | [] => constantSeries 1
    32 | S :: l => shuffle S (shuffleList l)
    33
    34noncomputable def shufflePow {X : Type} (S : NCSeries X) (n : ℕ) : NCSeries X :=
    35 shuffleList (List.replicate n S)
    36
    37axiom commutative {X : Type} (S T : NCSeries X) : shuffle S T = shuffle T S
    38
    39axiom associative {X : Type} (R S T : NCSeries X) :
    40 shuffle (shuffle R S) T = shuffle R (shuffle S T)
    41
    42axiom unit {X : Type} (S : NCSeries X) : shuffle (constantSeries 1) S = S
    43
    44end Lax825748.Shuffle
    45
    Show ProofShow 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…