Anti-derivatives of `P`-finite series

• Preliminaries
• Closure under left anti-derivatives
• Appendix
• References

Fix a product rule P and let Σ be an alphabet of size n. A series f is a left anti-derivative of series g₁, …, gₙ if for every aᵢ : Σ (with 1 ≤ i ≤ n), the left derivative of f with respect to aᵢ is gᵢ. We show that P-finite series are closed under anti-derivatives.

It is crucial that the input alphabet be finite. For this reason, we prove it in a module separate from FinitelyGenerated, since we need to reimport several definitions with a fixed finite alphabet.

{-# OPTIONS --guardedness --sized-types #-}

open import Preliminaries.Base renaming (_,,_ to _,_)
open import General.ProductRules

module General.FinitelyGenerated-AntiDerivatives
    (R : CommutativeRing)
    (n : ℕ) -- size of the alphabet
    (P : ProductRule R)
    where

open import Preliminaries.Vector
open import Preliminaries.Algebra R

Crucially, we fix the alphabet to be a finite set of size n.

Σ = Fin n

open import General.Series R Σ
open import General.Products R Σ
open import General.FinitelyGenerated R Σ P

open Product P

private variable
    m k : ℕ
    f g : A ⟪ Σ ⟫
    fs gs : Vec (A ⟪ Σ ⟫) m

Preliminaries

We will need the following two easy observations. First, the set of series generated by f ∷ fs includes at least all the series generated by fs.

∷-∈ : g ∈[ fs ] → g ∈[ f ∷ fs ]

The second statement is a generalisation of the previous one. If f is generated by fsᵢ, then f is generated by fs₁ ++ ⋯ ++ fsₙ.

concat-∈ : 
    {F : Vec (Vec (A ⟪ Σ ⟫) m) k} →
    f ∈[ fs ] →
    fs ∈ F →
    ------------------------------
    f ∈[ concat F ]

Closure under left anti-derivatives

We now show that P-finite series are closed under left anti-derivatives. More precisely, we show that, if all left derivatives δ f a of f are P-finite, then f itself is P-finite.

P-fin-δ⁻¹ :
    (∀ a → P-fin (δ f a) m) →
    --------------------------
    P-fin f ( +ℕ n +ℕ n *ℕ m)

For simplicity, we assume that δ f a is P-finite with m generators for every a : Σ. One could have the number of generators m depend on a, but this would complicate the notation without adding much insight. This is no loss of generality, since we can immagine that m is the maximum number of generators needed for any δ f a (which exists since the alphabet is finite).

The idea of the proof is to take as generators f itself, all its left derivatives δ f a (term δf below), and all the generators witnessing that the left derivatives are P-finite (term F below).

P-fin-δ⁻¹ {f} {m} ass =
    P-fin[ f ∷ δf ++ concat F , gen∈ (here refl) , lem ]
    where

    δf : Vec (A ⟪ Σ ⟫) n
    δf = tabulate $ δ f

    δfa∈δf : ∀ a → δ f a ∈ δf
    δfa∈δf = ∈-tabulate⁺ (δ f)

    gen′ : Σ → Vec (A ⟪ Σ ⟫) m
    gen′ a = gen $ ass a

    F : Vec (Vec (A ⟪ Σ ⟫) m) n
    F = tabulate gen′

    lem′ : ∀ {g a b} → g ∈[ gen′ b ] → δ g a ∈[ concat F ]
    lem′ {g} {a} {b} g∈[gen] = concat-∈ δga∈[gen] (∈-tabulate⁺ gen′ b)
        where

        δga∈[gen] : δ g a ∈[ gen′ b ]
        δga∈[gen] = δ-closed (ass b) a g∈[gen]

    lem :
        ∀ a {g} →
        g ∈ f ∷ δf ++ concat F →
        -----------------------------
        δ g a ∈[ f ∷ δf ++ concat F ]

    lem a {g} (here g≡f) rewrite g≡f = gen∈ $ there $ ∈-++⁺ˡ (δfa∈δf a)

    lem a {g} (there g∈δf++F)
        with ∈ᵥ-++ {a = g} {as = δf} {bs = concat F} g∈δf++F
    ... | inj₁ g∈δf
        with ∈-tabulate⁻ g∈δf
    lem a {g} (there g∈δf++F) | inj₁ g∈δf | b , g≡δfb
        = ∷-∈ $ ++-∈ʳ $ lem′ g∈[gen]
        where

        g∈[gen] : g ∈[ gen′ b ]
        g∈[gen] rewrite g≡δfb = memb (ass b)

    lem a {g} (there g∈δf++F) | inj₂ g∈concatF
        with concat-∈⁻ {ass = F} g∈concatF
    ... | gs , gs∈F , g∈gs
        with ∈-tabulate⁻ gs∈F
    ... | b , gs≡genb
        = ∷-∈ $ ++-∈ʳ $ lem′ g∈[gen]
        where

        g∈[gen] : g ∈[ gen′ b ]
        g∈[gen] rewrite gs≡genb = gen∈ g∈gs

Appendix

We conclude the section by proving the two preliminary claims.

∷-∈ 𝟘∈ = 𝟘∈
∷-∈ (gen∈ g∈fs) = gen∈ (there g∈fs)
∷-∈ (c ·∈ g∈[fs]) = c ·∈ ∷-∈ g∈[fs]
∷-∈ (f∈[fs] +∈ g∈[fs]) = ∷-∈ f∈[fs] +∈ ∷-∈ g∈[fs]
∷-∈ (f∈[fs] *∈ g∈[fs]) = ∷-∈ f∈[fs] *∈ ∷-∈ g∈[fs]
∷-∈ (f≈g ≈∈ g∈[fs]) = f≈g ≈∈ ∷-∈ g∈[fs]

concat-∈ f∈[fs] (here px) rewrite px = ++-∈ˡ f∈[fs]
concat-∈ {F = F} f∈[fs] (there fs∈F) with concat-∈ f∈[fs] fs∈F
... | f∈[F] = ++-∈ʳ f∈[F]

References