Powers of Hahn series and compatibility with coefficient scalars

Over a domain, taking a power multiplies the order and raises the leading coefficient to that power. These formulas detect whether a leading pole term can be cancelled by a power.

The order formula allows semiring coefficients; Mathlib's HahnSeries.addVal requires ring coefficients, so its AddValuation.map_pow does not cover this generality.

The formulas are TauCeti.hahnSeries_leadingCoeff_pow n and TauCeti.hahnSeries_orderTop_pow n; both are also simplification lemmas. The exponent is explicit, and the series is inferred from the equality being rewritten.

With the typeclasses below in scope, use the qualified names as follows:

example (f : HahnSeries Γ R) (n : ℕ) :
    (f ^ n).leadingCoeff = f.leadingCoeff ^ n :=
  TauCeti.hahnSeries_leadingCoeff_pow n (f := f)

example [Nontrivial R] (f : HahnSeries Γ R) (n : ℕ) :
    (f ^ n).orderTop = n • f.orderTop :=
  TauCeti.hahnSeries_orderTop_pow n (f := f)

This file also records that coefficientwise scalar multiplication associates and commutes with multiplication of Hahn series (TauCeti.hahnSeries_isScalarTower and TauCeti.hahnSeries_smulCommClass). Mathlib provides this for the action of Hahn series on Hahn modules, and for Hahn series through their algebra structure; but the default algebra structure on Laurent series R⸨X⸩ comes from R⟦X⟧ and is not definitionally the coefficientwise one, so for instance the R⸨X⸩-module structure on R-derivations of R⸨X⸩ needs this instance.

Finally, HahnModule.of_symm_smul' reads the coefficientwise action of R on HahnModule Γ R V through HahnModule.of, for the action instance underlying the R-module structure. HahnModule.ofLinearEquiv bundles this coefficient-preserving comparison as an R-linear equivalence. The lemmas HahnModule.coeff_smul_single_zero and HahnModule.single_smul_single_zero describe the convolution action of a scalar series on a constant module-valued series, coefficientwise and on monomials, and HahnModule.single_neg_smul_single_smul records that the monomials t ^ a and t ^ (-a) act inversely.

HahnSeries.coeff_mul_add_of_forall_le computes the coefficient of a product at the sum of lower bounds for the supports of the factors: it is the product of the coefficients at those bounds. The sum of the lower bounds bounds the support of the product (HahnSeries.add_le_of_mem_support_mul), and for powers HahnSeries.nsmul_le_of_mem_support_pow and HahnSeries.coeff_pow_nsmul_of_forall_le give the corresponding bound and coefficient. HahnSeries.zero_le_orderTop_single and HahnSeries.zero_le_orderTop_one record that monomials of nonnegative exponent, and in particular the constant 1, have nonnegative order.

instance TauCeti.hahnSeries_smulCommClass {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] : SMulCommClass R (HahnSeries Γ R) (HahnSeries Γ R)

Coefficientwise scalar multiplication commutes with multiplication of Hahn series.

instance TauCeti.hahnSeries_isScalarTower {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] : IsScalarTower R (HahnSeries Γ R) (HahnSeries Γ R)

Coefficientwise scalar multiplication associates with multiplication of Hahn series.

@[simp]

theorem TauCeti.hahnSeries_leadingCoeff_pow {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [NoZeroDivisors R] (n : ℕ) {f : HahnSeries Γ R} : (f ^ n).leadingCoeff = f.leadingCoeff ^ n

The leading coefficient of a power is the power of the leading coefficient.

@[simp]

theorem TauCeti.hahnSeries_orderTop_pow {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [NoZeroDivisors R] [Nontrivial R] (n : ℕ) {f : HahnSeries Γ R} : (f ^ n).orderTop = n • f.orderTop

The order of a power is the corresponding multiple of the order, including at zero.

@[simp]

theorem HahnModule.of_symm_smul' {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [PartialOrder Γ] [Monoid R] [AddMonoid V] [DistribMulAction R V] (r : R) (x : HahnModule Γ R V) : (of R).symm (r • x) = r • (of R).symm x

The coefficientwise scalar action underlying the R-module structure, read through of. Mathlib's HahnModule.of_symm_smul is stated for a different, though propositionally equal, scalar action instance, so it does not rewrite this one.

noncomputable def HahnModule.ofLinearEquiv (R : Type u_1) {Γ : Type u_2} {V : Type u_3} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] : HahnSeries Γ V ≃ₗ[R] HahnModule Γ R V

The coefficient-preserving comparison between Hahn series and Hahn modules, linear for the coefficientwise action of R.

@[simp]

theorem HahnModule.ofLinearEquiv_apply {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (f : HahnSeries Γ V) : (ofLinearEquiv R) f = (of R) f

@[simp]

theorem HahnModule.ofLinearEquiv_symm_apply {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (f : HahnModule Γ R V) : (ofLinearEquiv R).symm f = (of R).symm f

@[simp]

theorem HahnModule.coeff_smul_single_zero {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Zero R] [AddCommMonoid V] [SMulWithZero R V] (f : HahnSeries Γ R) (v : V) (g : Γ) : ((of R).symm (f • (of R) ((HahnSeries.single 0) v))).coeff g = f.coeff g • v

Multiplying a constant module-valued series by a scalar series multiplies each coefficient by the constant vector.

@[simp]

theorem HahnModule.single_neg_smul_single_smul {R : Type u_2} {V : Type u_3} {Γ : Type u_4} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Semiring R] [AddCommMonoid V] [Module R V] (a : Γ) (x : HahnModule Γ R V) : (HahnSeries.single (-a)) 1 • (HahnSeries.single a) 1 • x = x

Multiplying by the monomials t ^ a and then t ^ (-a) is the identity.

@[simp]

theorem HahnModule.single_smul_single_zero {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Zero R] [AddCommMonoid V] [SMulWithZero R V] (g : Γ) (r : R) (v : V) : (HahnSeries.single g) r • (of R) ((HahnSeries.single 0) v) = (of R) ((HahnSeries.single g) (r • v))

A scalar monomial times a constant vector series is a vector-valued monomial.

theorem HahnSeries.zero_le_orderTop_single {Γ : Type u_1} {R : Type u_2} [Zero Γ] [PartialOrder Γ] [Zero R] {a : Γ} (ha : 0 ≤ a) (r : R) : 0 ≤ ((single a) r).orderTop

A monomial of nonnegative exponent has nonnegative order.

theorem HahnSeries.zero_le_orderTop_one {Γ : Type u_1} {R : Type u_2} [Zero Γ] [PartialOrder Γ] [Zero R] [One R] : 0 ≤ orderTop 1

The constant 1 has nonnegative order.

theorem HahnSeries.coeff_mul_add_of_forall_le {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a b : Γ} (hx : ∀ i ∈ x.support, a ≤ i) (hy : ∀ j ∈ y.support, b ≤ j) : (x * y).coeff (a + b) = x.coeff a * y.coeff b

If x is supported at exponents at least a and y at exponents at least b, then the coefficient of x * y at a + b is the product of the coefficients at a and b.

theorem HahnSeries.add_le_of_mem_support_mul {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a b : Γ} (hx : ∀ i ∈ x.support, a ≤ i) (hy : ∀ j ∈ y.support, b ≤ j) (k : Γ) : k ∈ (x * y).support → a + b ≤ k

If x is supported at exponents at least a and y at exponents at least b, then x * y is supported at exponents at least a + b.

theorem HahnSeries.nsmul_le_of_mem_support_pow {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} {a : Γ} (hx : ∀ i ∈ x.support, a ≤ i) (n : ℕ) (i : Γ) : i ∈ (x ^ n).support → n • a ≤ i

If x is supported at exponents at least a, then x ^ n is supported at exponents at least n • a.

theorem HahnSeries.coeff_pow_nsmul_of_forall_le {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} {a : Γ} (hx : ∀ i ∈ x.support, a ≤ i) (n : ℕ) : (x ^ n).coeff (n • a) = x.coeff a ^ n

If x is supported at exponents at least a, then the coefficient of x ^ n at n • a is the n-th power of the coefficient of x at a.