Documentation

TauCeti.RingTheory.MvPowerSeries.Primitive.Basic

Termwise primitives of multivariate power series #

Over a commutative ℚ-algebra R, the termwise primitive of f = ∑ aᵥ Xᵛ with respect to the variable Xᵢ is

∫ f dXᵢ = ∑ aᵥ Xᵛ⁺ᵉⁱ / (νᵢ + 1).

It is a right inverse of the formal partial derivative ∂/∂Xᵢ, and it is the unique series with derivative f that has no terms free of Xᵢ. Rational scalars are needed to divide by νᵢ + 1: over a ring of characteristic p the series Xᵢ ^ (p - 1) is not a derivative, since the derivative of Xᵢ ^ p vanishes.

Main definitions #

Main results #

source
noncomputable def MvPowerSeries.primitive {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) :
MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The termwise primitive ∑ aᵥ Xᵛ ↦ ∑ aᵥ Xᵛ⁺ᵉⁱ / (νᵢ + 1) with respect to the variable Xᵢ, over a ℚ-algebra. Its coefficient at ν is aᵥ₋ₑᵢ / νᵢ, which is zero when νᵢ = 0.

Instances For
    source
    theorem MvPowerSeries.coeff_primitive {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
    (coeff n) ((primitive i) f) = (↑(n i))⁻¹ • (coeff (n - Finsupp.single i 1)) f

    The coefficient of the termwise primitive at ν is aᵥ₋ₑᵢ / νᵢ.

    source
    @[simp]
    theorem MvPowerSeries.coeff_primitive_of_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) (f : MvPowerSeries σ R) {n : σ →₀ ℕ} (h : n i = 0) :
    (coeff n) ((primitive i) f) = 0

    The termwise primitive with respect to Xᵢ has no terms free of Xᵢ.

    source
    @[simp]
    theorem MvPowerSeries.coeff_add_single_primitive {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
    (coeff (n + Finsupp.single i 1)) ((primitive i) f) = (↑(n i) + 1)⁻¹ • (coeff n) f

    The coefficient of the termwise primitive at ν + eᵢ is aᵥ / (νᵢ + 1).

    source
    @[simp]
    theorem MvPowerSeries.primitive_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) (n : σ →₀ ℕ) (a : R) :
    (primitive i) ((monomial n) a) = (monomial (n + Finsupp.single i 1)) ((↑(n i) + 1)⁻¹ • a)

    The termwise primitive of a monomial: ∫ a Xᵛ dXᵢ = a Xᵛ⁺ᵉⁱ / (νᵢ + 1).

    source
    @[simp]
    theorem MvPowerSeries.primitive_C {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) (a : R) :
    (primitive i) (C a) = (monomial (Finsupp.single i 1)) a

    The termwise primitive of a constant: ∫ a dXᵢ = a Xᵢ.

    source
    theorem MvPowerSeries.primitive_injective {σ : Type u_1} {R : Type u_2} [Semiring R] [Algebra ℚ R] (i : σ) :
    Function.Injective ⇑(primitive i)

    The termwise primitive with respect to Xᵢ is injective.

    source
    @[simp]
    theorem MvPowerSeries.pderiv_primitive {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Algebra ℚ R] (i : σ) (f : MvPowerSeries σ R) :
    (pderiv i) ((primitive i) f) = f

    The primitive is a right inverse of the derivative: ∂/∂Xᵢ (∫ f dXᵢ) = f.

    source
    @[simp]
    theorem MvPowerSeries.pderiv_primitive_of_ne {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Algebra ℚ R] {i j : σ} (hij : i ≠ j) (f : MvPowerSeries σ R) :
    (pderiv j) ((primitive i) f) = (primitive i) ((pderiv j) f)

    Differentiation in another variable commutes with termwise integration.

    source
    theorem MvPowerSeries.coeff_primitive_pderiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Algebra ℚ R] (i : σ) (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
    (coeff n) ((primitive i) ((pderiv i) f)) = if n i = 0 then 0 else (coeff n) f

    The primitive of a derivative: ∫ (∂f/∂Xᵢ) dXᵢ is f with its terms free of Xᵢ removed.

    source
    theorem MvPowerSeries.eq_primitive_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Algebra ℚ R] {i : σ} {f g : MvPowerSeries σ R} :
    g = (primitive i) f ↔ (pderiv i) g = f ∧ ∀ (n : σ →₀ ℕ), n i = 0 → (coeff n) g = 0

    Characterisation of the primitive: g = ∫ f dXᵢ iff ∂g/∂Xᵢ = f and g has no terms free of Xᵢ.