Lax Lean Archive

Multivariate constructible differentially algebraic power series

Lax619925.CDA · concepts/Lax619925/CDA.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

    Theorem

    An exponential multivariate power series in dd variables is a series f=Σnfnxn/n!f = Σ_n f_n x^n / n! (paper §6.4), identified with its coefficient sequence f:Nd→Qf : ℕ^d → ℚ. It carries a binomial-convolution product and commuting partial derivatives ∂xjf=Σnfn+ejxn/n!∂_{x_j} f = Σ_n f_{n+e_j} x^n / n! (the shift in the jj-th coordinate). A CDA system is a kk-tuple of such series satisfying ∂xjfi=pi(j)(f1,…,fk)∂_{x_j} f_i = p^{(j)}_i(f_1, …, f_k), the right-hand side a polynomial in the binomial-convolution algebra. The solvability problem asks whether, given the equations and an initial condition fi(0)=cif_i(0) = c_i, a solution exists. This is decidable (paper §6.4): the CDA system is isomorphic to a shuffle system over the dd-letter alphabet, so a solution exists exactly when the companion shuffle series are commutative, which is decidable.

    Concept map
    5 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 27 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Shuffle
    3import Mathlib.Data.Real.Basic
    4import Mathlib.Data.Fin.Basic
    5import Mathlib.Data.Fintype.Basic
    6import Mathlib.Data.Finset.Basic
    7import Mathlib.Data.Nat.Choose.Basic
    8import Mathlib.Algebra.MvPolynomial.Basic
    9
    10/-!
    11---
    12title: Multivariate constructible differentially algebraic power series
    13type: theorem
    14---
    15An *exponential multivariate power series* in `d` variables is a series
    16`f = Σ_n f_n x^n / n!` (paper §6.4), identified with its coefficient sequence
    17`f : ℕ^d → ℚ`. It carries a binomial-convolution product and commuting partial
    18derivatives `∂_{x_j} f = Σ_n f_{n+e_j} x^n / n!` (the shift in the `j`-th
    19coordinate). A *CDA system* is a `k`-tuple of such series satisfying
    20`∂_{x_j} f_i = p^{(j)}_i(f_1, …, f_k)`, the right-hand side a polynomial in the
    21binomial-convolution algebra. The *solvability problem* asks whether, given the
    22equations and an initial condition `f_i(0) = c_i`, a solution exists. This is
    23decidable (paper §6.4): the CDA system is isomorphic to a shuffle system over
    24the `d`-letter alphabet, so a solution exists exactly when the companion shuffle
    25series are commutative, which is decidable.
    26-/
    27
    28namespace Lax619925.CDA
    29
    30open Lax619925.Series Lax619925.Shuffle
    31
    32/-- An exponential multivariate power series in `d` variables, identified with
    33 its coefficient sequence (the series is `Σ_n f_n x^n / n!`). -/
    34abbrev ExpPowerSeries (d : ℕ) := (Fin d → ℕ) → ℚ
    35
    36/-- The binomial-convolution product of two exponential power series:
    37 `(expMul d f g) n = Σ_{m ≤ n} binom(n, m) f m · g (n - m)`, the product in the
    38 exponential (binomial) algebra, where the sum is over the multi-indices
    39 `m ≤ n` (coordinate-wise) and `binom(n, m) = ∏_i binom(n_i, m_i)` is the
    40 multinomial coefficient. -/
    41noncomputable def expMul (d : ℕ) (f g : ExpPowerSeries d) : ExpPowerSeries d :=
    42 fun n =>
    43 (Finset.univ.pi (fun i => Finset.range (n i + 1))).sum fun m =>
    44 let m' : Fin d → ℕ := fun i => m i (Finset.mem_univ i)
    45 (Finset.univ : Finset (Fin d)).prod (fun i => Nat.choose (n i) (m' i)) * f m' * g (fun i => n i - m' i)
    46
    47/-- The partial derivative in the `j`-th coordinate:
    48 `(expDeriv d j f) n = f (n + e_j)`. In the exponential normalisation this is
    49 the shift in the `j`-th coordinate; the partial derivatives commute. -/
    50def expDeriv (d : ℕ) (j : Fin d) (f : ExpPowerSeries d) : ExpPowerSeries d :=
    51 fun n => f (fun i => n i + if i = j then 1 else 0)
    52
    53/-- The `n`-fold binomial-convolution power of an exponential power series:
    54 `expPow d f 0` is the constant-1 series and `expPow d f (n+1) = expMul d (expPow d f n) f`. -/
    55noncomputable def expPow (d : ℕ) (f : ExpPowerSeries d) (n : ℕ) : ExpPowerSeries d :=
    56 match n with
    57 | 0 => fun idx => if idx = 0 then 1 else 0
    58 | n + 1 => expMul d (expPow d f n) f
    59
    60/-- The evaluation of the polynomial `p` at the tuple of exponential power series
    61 `fs`, in the binomial-convolution algebra: the variable `X_i` is mapped to
    62 `fs i` and the multiplication is the binomial-convolution product. -/
    63noncomputable def evalCDA (d k : ℕ) (fs : Fin k → ExpPowerSeries d) (p : MvPolynomial (Fin k) ℚ) :
    64 ExpPowerSeries d :=
    65 p.support.sum fun m =>
    66 p.coeff m • (Finset.univ : Finset (Fin k)).toList.foldr
    67 (fun i acc => expMul d acc (expPow d (fs i) (m i)))
    68 (fun idx => if idx = 0 then 1 else 0)
    69
    70/-- A `k`-tuple of exponential power series `f` *solves* the CDA system `(p, c)`
    71 if it satisfies the initial condition `f_i(0) = c_i` and the differential
    72 equations `∂_{x_j} f_i = p^{(j)}_i(f_1, …, f_k)` for all `i, j`, the
    73 right-hand side a polynomial in the binomial-convolution algebra. Here `0`
    74 is the zero multi-index. -/
    75def SolvesCDA (d k : ℕ) (f : Fin k → ExpPowerSeries d)
    76 (p : Fin k → Fin d → MvPolynomial (Fin k) ℚ) (c : Fin k → ℚ) : Prop :=
    77 (∀ i, f i 0 = c i) ∧ ∀ i j, expDeriv d j (f i) = evalCDA d k f (p i j)
    78
    79/-- The CDA solvability problem is decidable (paper §6.4, theorem `decidability
    80 of CDA solvability`): there is a procedure that, given the polynomial
    81 equations `p` and the initial condition `c`, decides whether a power series
    82 solution exists. The decision reduces to the commutativity of the companion
    83 shuffle series, which is decidable. -/
    84axiom CDASolvability (d k : ℕ) (hd : 0 < d) (hk : 0 < k) :
    85 ∃ dec : (Fin k → Fin d → MvPolynomial (Fin k) ℚ) → (Fin k → ℚ) → Bool,
    86 ∀ p c, dec p c = true ↔ ∃ f : Fin k → ExpPowerSeries d, SolvesCDA d k f p c
    87
    88end Lax619925.CDA
    89
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…