Documentation

AlgebraicCombinatorics.FPS.Substitution

Substitution and Evaluation of Power Series #

This file formalizes the theory of substitution (composition) of formal power series (FPS).

Main definitions #

Main results #

Implementation notes #

In Mathlib, the substitution f[g] is denoted PowerSeries.subst g f (note the order reversal). The condition for substitution is PowerSeries.HasSubst g, which requires the constant coefficient of g to be nilpotent. For power series over a reduced ring (like a field), this is equivalent to having constant term 0.

The source text uses the notation f[g] for substituting g into f, which corresponds to PowerSeries.subst g f in Mathlib.

References #

Section: Defining substitution #

Definition 7.3.1 (def.fps.subs): Let f and g be two FPSs in K⟦x⟧. Assume that [x⁰]g = 0. We define f[g] := ∑_{n∈ℕ} fₙ gⁿ.

In Mathlib, this is PowerSeries.subst g f when PowerSeries.HasSubst g holds. The condition [x⁰]g = 0 implies HasSubst g via HasSubst.of_constantCoeff_zero'.

source
noncomputable def AlgebraicCombinatorics.fps_comp {K : Type u_1} [CommRing K] (f g : PowerSeries K) (_hg : PowerSeries.constantCoeff g = 0) :
PowerSeries K

Definition 7.3.1 (def.fps.subs) The composition/substitution f[g] of power series is defined when g has constant term 0. This is the Mathlib PowerSeries.subst function.

Equations
Instances For
    source
    theorem AlgebraicCombinatorics.fps_comp_eq_subst {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    fps_comp f g hg = PowerSeries.subst g f

    The composition f[g] equals the Mathlib substitution.

    source
    theorem AlgebraicCombinatorics.fps_comp_coeff {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (n : ℕ) :
    (PowerSeries.coeff n) (PowerSeries.subst g f) = ∑ᶠ (d : ℕ), (PowerSeries.coeff d) f * (PowerSeries.coeff n) (g ^ d)

    Definition 7.3.1 (def.fps.subs) - Coefficient formula The n-th coefficient of f[g] is the (finitely supported) sum ∑_{d∈ℕ} fₐ · xⁿ.

    This is the explicit formula from Definition 7.3.1: f[g] = ∑_{n∈ℕ} fₙ gⁿ, expressed at the coefficient level.

    Section: Well-definedness (Proposition 7.3.3) #

    Proposition 7.3.3 (prop.fps.subs.wd): Let f and g be two FPSs with [x⁰]g = 0. (a) For each n∈ℕ, the first n coefficients of g^n are 0. (b) The sum ∑{n∈ℕ} fₙ gⁿ is well-defined. (c) [x⁰](∑{n∈ℕ} fₙ gⁿ) = f₀.

    source
    theorem AlgebraicCombinatorics.fps_subs_wd_firstCoeffs {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (n k : ℕ) (hk : k < n) :
    (PowerSeries.coeff k) (g ^ n) = 0

    Proposition 7.3.3(a) (prop.fps.subs.wd) For each n∈ℕ, the first n coefficients of the FPS g^n are 0 when g has constant term 0.

    This follows from g = x·h for some h, so g^n = x^n · h^n.

    source
    theorem AlgebraicCombinatorics.fps_comp_coeff_finite {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (n : ℕ) :
    (PowerSeries.coeff n) (PowerSeries.subst g f) = ∑ d ∈ Finset.range (n + 1), (PowerSeries.coeff d) f * (PowerSeries.coeff n) (g ^ d)

    Definition 7.3.1 (def.fps.subs) - Alternative coefficient formula For any fixed n, the sum ∑_{d∈ℕ} fₐ · xⁿ is actually finite, since xⁿ = 0 for d > n when g has constant term 0.

    source
    theorem AlgebraicCombinatorics.fps_subs_wd_summable {K : Type u_1} [CommRing K] (_f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.HasSubst g

    Proposition 7.3.3(b) (prop.fps.subs.wd) The family (fₙ gⁿ)_{n∈ℕ} is summable, i.e., for each coefficient position m, only finitely many terms contribute.

    In Mathlib, this is built into the definition of PowerSeries.subst via HasSubst.

    source
    theorem AlgebraicCombinatorics.fps_subs_wd_constCoeff {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.constantCoeff (PowerSeries.subst g f) = PowerSeries.constantCoeff f

    Proposition 7.3.3(c) (prop.fps.subs.wd) The constant coefficient of f[g] equals f₀.

    source
    @[simp]
    theorem AlgebraicCombinatorics.subst_zero {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g 0 = 0

    Substituting into 0 gives 0.

    source
    @[simp]
    theorem AlgebraicCombinatorics.subst_one {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g 1 = 1

    Substituting into 1 gives 1.

    Section: Lemma for first k coefficients (Lemma 7.3.5) #

    Lemma 7.3.5 (lem.fps.fg-coeffs-0): Let f, g ∈ K⟦x⟧ with [x⁰]g = 0. If the first k coefficients of f are 0, then the first k coefficients of f ∘ g are 0.

    source
    theorem AlgebraicCombinatorics.fps_fg_coeffs_zero {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (k : ℕ) (hf : ∀ m < k, (PowerSeries.coeff m) f = 0) (m : ℕ) :
    m < k → (PowerSeries.coeff m) (PowerSeries.subst g f) = 0

    Lemma 7.3.5 (lem.fps.fg-coeffs-0) If the first k coefficients of f are 0, then the first k coefficients of f ∘ g are 0.

    Section: Laws of substitution (Proposition 7.3.4) #

    Proposition 7.3.4 (prop.fps.subs.rules): Composition of FPSs satisfies expected rules.

    source
    theorem AlgebraicCombinatorics.fps_subs_add {K : Type u_1} [CommRing K] (f₁ f₂ g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g (f₁ + f₂) = PowerSeries.subst g f₁ + PowerSeries.subst g f₂

    Proposition 7.3.4(a) (prop.fps.subs.rules) (f₁ + f₂) ∘ g = f₁ ∘ g + f₂ ∘ g

    source
    theorem AlgebraicCombinatorics.fps_subs_mul {K : Type u_1} [CommRing K] (f₁ f₂ g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g (f₁ * f₂) = PowerSeries.subst g f₁ * PowerSeries.subst g f₂

    Proposition 7.3.4(b) (prop.fps.subs.rules) (f₁ · f₂) ∘ g = (f₁ ∘ g) · (f₂ ∘ g)

    source
    theorem AlgebraicCombinatorics.fps_subs_div {K : Type u_2} [Field K] (f₁ f₂ g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (hf₂ : PowerSeries.constantCoeff f₂ ≠ 0) :
    PowerSeries.subst g f₁ * (PowerSeries.subst g f₂)⁻¹ = PowerSeries.subst g (f₁ * f₂⁻¹)

    Proposition 7.3.4(c) (prop.fps.subs.rules) (f₁ / f₂) ∘ g = (f₁ ∘ g) / (f₂ ∘ g) when f₂ is invertible.

    Note: Division of power series requires working over a field. We state this for the case where K is a field and f₂ has nonzero constant coefficient.

    In the source, this is stated as: if f₂ is invertible (i.e., has nonzero constant term), then f₂ ∘ g is automatically invertible and the division rule holds.

    source
    theorem AlgebraicCombinatorics.fps_subs_pow {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (k : ℕ) :
    PowerSeries.subst g (f ^ k) = PowerSeries.subst g f ^ k

    Proposition 7.3.4(d) (prop.fps.subs.rules) f^k ∘ g = (f ∘ g)^k

    source
    theorem AlgebraicCombinatorics.fps_subs_assoc_constCoeff {K : Type u_1} [CommRing K] (g h : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (hh : PowerSeries.constantCoeff h = 0) :
    PowerSeries.constantCoeff (PowerSeries.subst h g) = 0

    Proposition 7.3.4(e) (prop.fps.subs.rules) (f ∘ g) ∘ h = f ∘ (g ∘ h), and [x⁰](g ∘ h) = 0.

    Part 1: The constant coefficient of g ∘ h is 0.

    source
    theorem AlgebraicCombinatorics.fps_subs_assoc {K : Type u_1} [CommRing K] (f g h : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (hh : PowerSeries.constantCoeff h = 0) :
    PowerSeries.subst h (PowerSeries.subst g f) = PowerSeries.subst (PowerSeries.subst h g) f

    Proposition 7.3.4(e) (prop.fps.subs.rules) (f ∘ g) ∘ h = f ∘ (g ∘ h)

    Part 2: Associativity of composition.

    source
    theorem AlgebraicCombinatorics.fps_subs_const {K : Type u_1} [CommRing K] (a : K) (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g (PowerSeries.C a) = PowerSeries.C a

    Proposition 7.3.4(f) (prop.fps.subs.rules) a ∘ g = a for any constant a ∈ K.

    source
    theorem AlgebraicCombinatorics.fps_subs_X_left {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g PowerSeries.X = g

    Proposition 7.3.4(g) (prop.fps.subs.rules) X ∘ g = g

    source
    @[simp]
    theorem AlgebraicCombinatorics.subst_X' {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g PowerSeries.X = g

    Substituting X into g gives g back. Simp-lemma alias for fps_subs_X_left.

    source
    theorem AlgebraicCombinatorics.fps_subs_X_right {K : Type u_1} [CommRing K] (g : PowerSeries K) :
    PowerSeries.subst PowerSeries.X g = g

    Proposition 7.3.4(g) (prop.fps.subs.rules) g ∘ X = g

    source
    theorem AlgebraicCombinatorics.fps_subs_sum {K : Type u_1} [CommRing K] {ι : Type u_2} (s : Finset ι) (f : ι → PowerSeries K) (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) :
    PowerSeries.subst g (∑ i ∈ s, f i) = ∑ i ∈ s, PowerSeries.subst g (f i)

    Proposition 7.3.4(h) (prop.fps.subs.rules) - Finite sum version For a finite sum (∑ᵢ∈s fᵢ), we have (∑ᵢ∈s fᵢ) ∘ g = ∑ᵢ∈s (fᵢ ∘ g).

    Infinite sum version of Proposition 7.3.4(h) #

    For the full statement of Proposition 7.3.4(h), we need to work with summable families of FPS in the sense of Definition def.fps.summable: a family (fᵢ)_{i∈I} is summable if for each coefficient index n, all but finitely many i have [x^n]fᵢ = 0.

    Note: SummableFPS, summableFPSSum, and coeff_summableFPSSum are imported from FPSDefinition.lean, which is the canonical location for these definitions.

    source
    theorem AlgebraicCombinatorics.fps_subs_summable {K : Type u_1} [CommRing K] {ι : Type u_2} (f : ι → PowerSeries K) (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (hf : FPS.SummableFPS f) :
    FPS.SummableFPS fun (i : ι) => PowerSeries.subst g (f i)

    Proposition 7.3.4(h) (prop.fps.subs.rules) - Summability preservation If (fᵢ){i∈I} is a summable family and g has constant term 0, then (fᵢ ∘ g){i∈I} is also summable.

    The key insight is that [x^n](fᵢ ∘ g) only depends on [x^0]fᵢ, ..., [x^n]fᵢ. If all these are 0, then [x^n](fᵢ ∘ g) = 0. So the set of i with [x^n](fᵢ ∘ g) ≠ 0 is contained in the finite union ⋃_{k≤n} {i | [x^k]fᵢ ≠ 0}.

    source
    theorem AlgebraicCombinatorics.fps_subs_summableFPSSum {K : Type u_1} [CommRing K] {ι : Type u_2} (f : ι → PowerSeries K) (g : PowerSeries K) (hg : PowerSeries.constantCoeff g = 0) (hf : FPS.SummableFPS f) :
    PowerSeries.subst g (FPS.summableFPSSum f hf) = FPS.summableFPSSum (fun (i : ι) => PowerSeries.subst g (f i)) ⋯

    Proposition 7.3.4(h) (prop.fps.subs.rules) - Infinite sum version For a summable family (fᵢ)_{i∈I}, we have (∑ᵢ fᵢ) ∘ g = ∑ᵢ (fᵢ ∘ g).

    This is the full infinite sum version of the substitution rule. The proof uses the distributive law for multiplication over infinite sums and Fubini's theorem for essentially finite double sums.

    Section: Examples #

    Example 7.3.2 (exa.fps.subs.fibonacci): Substituting x + x² into 1/(1-x) gives the generating function for shifted Fibonacci numbers.

    source
    noncomputable def AlgebraicCombinatorics.geometricSeries {K : Type u_2} [Field K] :
    PowerSeries K

    The geometric series 1 + x + x² + ... = 1/(1-x)

    Equations
    Instances For
      source
      theorem AlgebraicCombinatorics.fps_geometric_subst_fibonacci {K : Type u_2} [Field K] :
      PowerSeries.subst (PowerSeries.X + PowerSeries.X ^ 2) geometricSeries = (1 - PowerSeries.X - PowerSeries.X ^ 2)⁻¹

      Substituting (x + x²) into the geometric series yields 1/(1 - x - x²). This is related to the Fibonacci generating function.

      The proof uses Proposition 7.3.4(c): (1/f₂)[g] = 1[g] / f₂[g] = 1 / f₂[g].

      Note: The full proof requires showing that subst preserves inverses when the original power series has invertible constant coefficient.

      Section: Kronecker delta notation (Definition 7.3.6) #

      Definition 7.3.6 (def.kron-delta): The Kronecker delta δᵢⱼ is 1 if i = j, 0 otherwise. This is used in the proofs but is standard notation.

      The Kronecker delta is defined as:

      δᵢⱼ = 1  if i = j
δᵢⱼ = 0  if i ≠ j

      For example, δ₂₂ = 1 and δ₃₈ = 0.

      source
      def AlgebraicCombinatorics.kroneckerDelta {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] (i j : α) :
      K

      Definition 7.3.6 (def.kron-delta) The Kronecker delta function: δᵢⱼ is 1 if i = j, and 0 otherwise.

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicCombinatorics.kroneckerDelta_self {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] (i : α) :
        kroneckerDelta i i = 1

        δᵢᵢ = 1

        source
        @[simp]
        theorem AlgebraicCombinatorics.kroneckerDelta_ne {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] {i j : α} (h : i ≠ j) :
        kroneckerDelta i j = 0

        δᵢⱼ = 0 when i ≠ j

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_comm {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] (i j : α) :
        kroneckerDelta i j = kroneckerDelta j i

        Symmetry: δᵢⱼ = δⱼᵢ

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_mul_left {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] (i j : α) (a : K) :
        kroneckerDelta i j * a = if i = j then a else 0

        Multiplication on the left: δᵢⱼ · a = a if i = j, else 0

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_mul_right {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] (i j : α) (a : K) :
        a * kroneckerDelta i j = if i = j then a else 0

        Multiplication on the right: a · δᵢⱼ = a if i = j, else 0

        source
        theorem AlgebraicCombinatorics.sum_kroneckerDelta_left {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Fintype α] (j : α) :
        ∑ i : α, kroneckerDelta i j = 1

        Sum over the first index: ∑ᵢ δᵢⱼ = 1

        source
        theorem AlgebraicCombinatorics.sum_kroneckerDelta_right {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Fintype α] (i : α) :
        ∑ j : α, kroneckerDelta i j = 1

        Sum over the second index: ∑ⱼ δᵢⱼ = 1

        source
        theorem AlgebraicCombinatorics.sum_kroneckerDelta_mul {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Fintype α] (j : α) (f : α → K) :
        ∑ i : α, kroneckerDelta i j * f i = f j

        Contraction/selection property: ∑ᵢ δᵢⱼ · f(i) = f(j)

        This is the key property that makes Kronecker delta useful: summing over one index "selects" the value at the other index.

        source
        theorem AlgebraicCombinatorics.sum_mul_kroneckerDelta {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Fintype α] (i : α) (f : α → K) :
        ∑ j : α, f j * kroneckerDelta i j = f i

        Contraction/selection property (variant): ∑ⱼ f(j) · δᵢⱼ = f(i)

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_nat_eq {K : Type u_1} [CommRing K] {n m : ℕ} :
        kroneckerDelta n m = if n = m then 1 else 0

        Kronecker delta for natural numbers (explicit form)

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_int_eq {K : Type u_1} [CommRing K] {n m : ℤ} :
        kroneckerDelta n m = if n = m then 1 else 0

        Kronecker delta for integers (explicit form)

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_eq_zero_iff {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Nontrivial K] {i j : α} :
        kroneckerDelta i j = 0 ↔ i ≠ j

        Kronecker delta equals zero iff the indices are different

        source
        theorem AlgebraicCombinatorics.kroneckerDelta_eq_one_iff {K : Type u_1} [CommRing K] {α : Type u_2} [DecidableEq α] [Nontrivial K] {i j : α} :
        kroneckerDelta i j = 1 ↔ i = j

        Kronecker delta equals one iff the indices are equal (when 1 ≠ 0)