Self-multiplication cancellation and orders of power series

A formal power series fixed by multiplication with a series of zero constant coefficient is zero: if f = g * f in R⟦X⟧ and constantCoeff g = 0, then f = 0.

This is the uniqueness engine for recursively defined power series: two solutions of the same recurrence have a difference f satisfying exactly such a fixed-point equation, with the g coming from the recurrence and having no constant term.

Multiplication on either side works, and neither form needs commutativity.

An injective map of coefficient semirings preserves the order of a power series: it sends nonzero coefficients to nonzero coefficients. Mathlib records only the inequality PowerSeries.le_order_map.

Power series constructed degree by degree are limits of approximations whose consecutive terms agree in more and more low degrees; PowerSeries.exists_forall_le_order_sub supplies the limit.

A series X ^ k * f with constantCoeff f ≠ 0 has order exactly k, over any semiring.

Main results

• PowerSeries.eq_zero_of_self_eq_mul_self: constantCoeff g = 0 and f = g * f give f = 0.

• PowerSeries.eq_zero_of_self_eq_self_mul: the same for f = f * g.

• PowerSeries.order_map_of_injective: injective coefficient maps preserve orders.

• PowerSeries.exists_forall_le_order_sub: a sequence whose consecutive terms agree below degree n has a limit agreeing with its n-th term below degree n.

• PowerSeries.order_X_pow_mul_of_constantCoeff_ne_zero: X ^ k * f has order k when f has nonzero constant coefficient.

Provenance

Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/PowerSeriesHelpers.lean, declarations eq_zero_of_self_eq_mul_self and eq_zero_of_self_eq_self_mul. The source states the second over a CommSemiring, deriving it from the first by mul_comm; that hypothesis is unnecessary, and both are stated here over a Semiring.

theorem PowerSeries.eq_zero_of_self_eq_mul_self {R : Type u_1} [Semiring R] {f g : PowerSeries R} (hg : constantCoeff g = 0) (h : f = g * f) : f = 0

Self-multiplication cancellation. If f = g * f in R⟦X⟧ and g has zero constant coefficient, then f = 0.

theorem PowerSeries.eq_zero_of_self_eq_self_mul {R : Type u_1} [Semiring R] {f g : PowerSeries R} (hg : constantCoeff g = 0) (h : f = f * g) : f = 0

Self-multiplication cancellation, other side. If f = f * g in R⟦X⟧ and g has zero constant coefficient, then f = 0.

No commutativity is needed: order f + order g ≤ order (f * g) holds with the factors in either order, so this runs the same argument as eq_zero_of_self_eq_mul_self.

@[simp]

theorem PowerSeries.order_map_of_injective {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : PowerSeries R) : ((map φ) f).order = f.order

An injective map of coefficient semirings preserves the order of a power series.

theorem PowerSeries.exists_forall_le_order_sub {R : Type u_2} [Ring R] {f : ℕ → PowerSeries R} (hf : ∀ (n : ℕ), ↑n ≤ (f (n + 1) - f n).order) : ∃ (g : PowerSeries R), ∀ (n : ℕ), ↑n ≤ (g - f n).order

Limits of X-adic Cauchy sequences. If consecutive terms of a sequence of power series agree below degree n, then there is a power series agreeing with its n-th term below degree n for every n.

theorem PowerSeries.order_X_pow_mul_of_constantCoeff_ne_zero {R : Type u_1} [Semiring R] {f : PowerSeries R} (hf : constantCoeff f ≠ 0) (k : ℕ) : (X ^ k * f).order = ↑k

Multiplying a power series with nonzero constant coefficient by X ^ k gives a series of order exactly k.