Lowest-degree homogeneous components of powers, products and substitutions

If a series has order at least p, the degree-n * p homogeneous component of its n-th power is the n-th power of its degree-p component, and similarly for finite products. This reduces lowest-degree coefficient computations for powers to homogeneous series, over arbitrary semirings.

The same holds for substitution: if f has order at least p and the series a i have zero constant coefficient, the degree-p component of f(a) only depends on the degree-p component of f and on the linear parts of the a i, into which it is substituted (MvPowerSeries.homogeneousComponent_subst_of_le_order). This is how the lowest-degree term of an expression such as f(F(X, Y), Z), for a formal group law F(X, Y) = X + Y + ⋯, is read off as the polynomial f_p(X + Y, Z). In finitely many variables the degree-p component is a polynomial (MvPowerSeries.homogeneousComponentPolynomial), and the lowest-degree component of f(a) is that polynomial evaluated at the linear parts of the a i (MvPowerSeries.homogeneousComponent_subst_eq_coe_aeval).

Products and powers of close series are close: the order of x y - x' y' is bounded through those of x - x' and y - y' (MvPowerSeries.le_order_mul_sub_mul), and if x and y have zero constant coefficient and x - y has order at least n, then xᵏ - yᵏ has order at least n + k - 1 (MvPowerSeries.le_order_pow_sub_pow). Substitution is Lipschitz for the order: if every a i and b i has zero constant coefficient and a i - b i has order at least n for all i, then f(a) - f(b) has order at least n + k - 1 when f has order at least k (MvPowerSeries.le_order_subst_sub_subst), and under the same hypotheses, in degrees at most n it agrees with the linear part ∑ᵢ fᵢ (a i - b i) of f applied to the differences (MvPowerSeries.coeff_subst_sub_subst_of_degree_le).

Perturbing one entry a s by a series e of order at least n ≥ 1 changes f(a) by c e, where c is the coefficient of Xₛ in f, up to terms of degree greater than n (MvPowerSeries.le_order_subst_update_add_sub). For a formal group law this says that F(x + e, y) ≡ F(x, y) + e to lowest order. The proof uses that below degree n + 1, multiplying e by a series q scales it by the constant coefficient of q (MvPowerSeries.coeff_mul_eq_coeff_mul_constantCoeff_of_le_order).

A common lower bound on the orders of two series bounds the orders of their sum and difference (MvPowerSeries.le_order_add, MvPowerSeries.le_order_sub). Over a commutative ring, if f and g have zero constant coefficient, then f ^ n - g ^ n has order larger than that of f - g for n ≥ 2 (MvPowerSeries.order_sub_add_one_le_order_pow_sub_pow). The degree-zero component of a series is its constant term (MvPowerSeries.homogeneousComponent_zero).

For two-variable series with linear coefficients one, the degree-one component is X + Y. Over a ring, vanishing of the constant coefficient then puts the remainder after subtracting X + Y in order at least two, and over a commutative ring the linear part of f(x, y) is the sum of the linear parts of x and y (MvPowerSeries.homogeneousComponent_one_subst_pair).

theorem MvPowerSeries.le_order_iff {σ : Type u_1} {R : Type u_2} {n : ℕ∞} [Semiring R] {f : MvPowerSeries σ R} : n ≤ f.order ↔ ∀ (d : σ →₀ ℕ), ↑(Finsupp.degree d) < n → (coeff d) f = 0

A power series has order at least n exactly when all its coefficients in total degree less than n vanish.

theorem MvPowerSeries.le_order_add {σ : Type u_1} {R : Type u_2} {n : ℕ∞} [Semiring R] {f g : MvPowerSeries σ R} (hf : n ≤ f.order) (hg : n ≤ g.order) : n ≤ (f + g).order

A lower bound on the orders of two series bounds the order of their sum.

theorem MvPowerSeries.le_order_sub {σ : Type u_1} {R : Type u_2} {n : ℕ∞} [Ring R] {f g : MvPowerSeries σ R} (hf : n ≤ f.order) (hg : n ≤ g.order) : n ≤ (f - g).order

A lower bound on the orders of two series bounds the order of their difference.

theorem MvPowerSeries.order_sub_add_one_le_order_pow_sub_pow {σ : Type u_1} {R : Type u_2} [CommRing R] {f g : MvPowerSeries σ R} (hf : constantCoeff f = 0) (hg : constantCoeff g = 0) {n : ℕ} (hn : 2 ≤ n) : (f - g).order + 1 ≤ (f ^ n - g ^ n).order

If f and g have zero constant coefficient and 2 ≤ n, then the order of f ^ n - g ^ n exceeds that of f - g: it is f - g times ∑ fⁱ gⁿ⁻¹⁻ⁱ, whose constant coefficient vanishes.

@[simp]

theorem MvPowerSeries.homogeneousComponent_one_X {σ : Type u_1} {R : Type u_2} [Semiring R] (i : σ) : (homogeneousComponent 1) (X i) = X i

A variable is its own degree-one homogeneous component.

theorem MvPowerSeries.homogeneousComponent_one_eq_C_mul_X {R : Type u_2} [Semiring R] (f : MvPowerSeries Unit R) : (homogeneousComponent 1) f = C ((coeff (Finsupp.single () 1)) f) * X ()

In one variable, the degree-one homogeneous component of f is c X, where c is the coefficient of X in f.

@[simp]

theorem MvPowerSeries.constantCoeff_homogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] {p : ℕ} (hp : p ≠ 0) (f : MvPowerSeries σ R) : constantCoeff ((homogeneousComponent p) f) = 0

A homogeneous component of positive degree has no constant coefficient.

theorem MvPowerSeries.succ_le_order_of_homogeneousComponent_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {n : ℕ} (hn : ↑n ≤ f.order) (h : (homogeneousComponent n) f = 0) : ↑(n + 1) ≤ f.order

A series of order at least n without degree-n component has order at least n + 1.

theorem MvPowerSeries.homogeneousComponent_pow_of_le_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p ≤ f.order) (n : ℕ) : (homogeneousComponent (n * p)) (f ^ n) = (homogeneousComponent p) f ^ n

The lowest possible homogeneous component of a power is the corresponding power of the lowest possible homogeneous component.

theorem MvPowerSeries.homogeneousComponent_pow_of_constantCoeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} (hf : constantCoeff f = 0) (n : ℕ) : (homogeneousComponent n) (f ^ n) = (homogeneousComponent 1) f ^ n

For a series without constant coefficient, the degree-n component of its n-th power is the n-th power of its linear part.

@[simp]

theorem MvPowerSeries.homogeneousComponent_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) : (homogeneousComponent 0) f = C (constantCoeff f)

The degree-zero homogeneous component of a power series is its constant term.

theorem MvPowerSeries.homogeneousComponent_prod_of_le_order {σ : Type u_1} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (s : Finset ι) {f : ι → MvPowerSeries σ R} {p : ι → ℕ} (hf : ∀ i ∈ s, ↑(p i) ≤ (f i).order) : (homogeneousComponent (∑ i ∈ s, p i)) (∏ i ∈ s, f i) = ∏ i ∈ s, (homogeneousComponent (p i)) (f i)

The lowest possible homogeneous component of a finite product is the product of the lowest possible homogeneous components of the factors.

theorem MvPowerSeries.degree_le_order_prod_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {a : ι → MvPowerSeries σ R} (ha₀ : ∀ (i : ι), constantCoeff (a i) = 0) (d : ι →₀ ℕ) : ↑(Finsupp.degree d) ≤ (d.prod fun (i : ι) (k : ℕ) => a i ^ k).order

The monomial aᵈ = ∏ᵢ (a i) ^ (d i) in series without constant coefficient has order at least the degree of d.

theorem MvPowerSeries.homogeneousComponent_degree_prod_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {a : ι → MvPowerSeries σ R} (ha₀ : ∀ (i : ι), constantCoeff (a i) = 0) (d : ι →₀ ℕ) : (homogeneousComponent (Finsupp.degree d)) (d.prod fun (i : ι) (k : ℕ) => a i ^ k) = d.prod fun (i : ι) (k : ℕ) => (homogeneousComponent 1) (a i) ^ k

The degree-|d| component of the monomial aᵈ = ∏ᵢ (a i) ^ (d i) in series without constant coefficient is the same monomial in their linear parts.

theorem MvPowerSeries.HasSubst.homogeneousComponent_one {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [CommRing S] {a : σ → MvPowerSeries τ S} (ha : HasSubst a) : HasSubst fun (i : σ) => (homogeneousComponent 1) (a i)

The linear parts of a substitutable family can be substituted.

theorem MvPowerSeries.homogeneousComponent_subst_of_le_order {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p ≤ f.order) {a : σ → MvPowerSeries τ S} (ha : HasSubst a) (ha₀ : ∀ (i : σ), constantCoeff (a i) = 0) : (homogeneousComponent p) (subst a f) = subst (fun (i : σ) => (homogeneousComponent 1) (a i)) ((homogeneousComponent p) f)

The lowest-degree component of a substitution. If f has order at least p and the series a i have zero constant coefficient, the degree-p component of f(a) is the degree-p component of f evaluated at the linear parts of the a i.

noncomputable def MvPowerSeries.homogeneousComponentPolynomial {σ : Type u_1} {R : Type u_3} [Finite σ] [CommSemiring R] (n : ℕ) (f : MvPowerSeries σ R) : MvPolynomial σ R

The degree-n homogeneous component of a power series in finitely many variables, as a polynomial.

@[simp]

theorem MvPowerSeries.coe_homogeneousComponentPolynomial {σ : Type u_1} {R : Type u_3} [Finite σ] [CommSemiring R] (n : ℕ) (f : MvPowerSeries σ R) : ↑(homogeneousComponentPolynomial n f) = (homogeneousComponent n) f

theorem MvPowerSeries.isHomogeneous_homogeneousComponentPolynomial {σ : Type u_1} {R : Type u_3} [Finite σ] [CommSemiring R] (n : ℕ) (f : MvPowerSeries σ R) : (homogeneousComponentPolynomial n f).IsHomogeneous n

theorem MvPowerSeries.homogeneousComponent_subst_eq_coe_aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [Finite σ] [CommRing R] {n : ℕ} {f : MvPowerSeries σ R} (hn : ↑n ≤ f.order) {a : σ → MvPowerSeries τ R} (ha : HasSubst a) (ha₀ : ∀ (i : σ), constantCoeff (a i) = 0) {l : σ → MvPolynomial τ R} (hl : ∀ (i : σ), (homogeneousComponent 1) (a i) = ↑(l i)) : (homogeneousComponent n) (subst a f) = ↑((MvPolynomial.aeval l) (homogeneousComponentPolynomial n f))

If f vanishes below degree n and the series a i have no constant term, the degree-n part of f(a) is the polynomial degree-n part of f evaluated at polynomials l i equal to the linear parts of the a i.

theorem MvPowerSeries.le_order_mul_sub_mul {τ : Type u_2} {R : Type u_3} [Ring R] {x x' y y' : MvPowerSeries τ R} {m : ℕ∞} (h₁ : m ≤ (x - x').order + y.order) (h₂ : m ≤ x'.order + (y - y').order) : m ≤ (x * y - x' * y').order

The order of x y - x' y' is at least the smaller of the orders of (x - x') y and x' (y - y').

theorem MvPowerSeries.le_order_pow_sub_pow {τ : Type u_2} {R : Type u_3} {n : ℕ} [Ring R] {x y : MvPowerSeries τ R} (hx : constantCoeff x = 0) (hy : constantCoeff y = 0) (hxy : ↑n ≤ (x - y).order) {k : ℕ} : ↑(n + k - 1) ≤ (x ^ k - y ^ k).order

If x - y has order at least n and x, y have zero constant coefficient, then xᵏ - yᵏ has order at least n + k - 1.

theorem MvPowerSeries.le_order_prod_pow_sub_prod_pow {τ : Type u_2} {R : Type u_3} {n : ℕ} [CommRing R] {ι : Type u_4} {a b : ι → MvPowerSeries τ R} (ha₀ : ∀ (i : ι), constantCoeff (a i) = 0) (hb₀ : ∀ (i : ι), constantCoeff (b i) = 0) (hab : ∀ (i : ι), ↑n ≤ (a i - b i).order) (d : ι →₀ ℕ) : ↑(n + Finsupp.degree d - 1) ≤ ((d.prod fun (i : ι) (k : ℕ) => a i ^ k) - d.prod fun (i : ι) (k : ℕ) => b i ^ k).order

Monomials in close arguments are closer. If the series a i and b i have zero constant coefficient and a i - b i has order at least n for every i, then the monomials aᵈ and bᵈ differ by a series of order at least n + |d| - 1.

theorem MvPowerSeries.le_order_subst_sub_subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {n : ℕ} [CommRing R] {H : MvPowerSeries σ R} {k : ℕ} (hH : ↑k ≤ H.order) {a b : σ → MvPowerSeries τ R} (ha : HasSubst a) (hb : HasSubst b) (ha₀ : ∀ (i : σ), constantCoeff (a i) = 0) (hb₀ : ∀ (i : σ), constantCoeff (b i) = 0) (hab : ∀ (i : σ), ↑n ≤ (a i - b i).order) : ↑(n + k - 1) ≤ (subst a H - subst b H).order

Substitution is Lipschitz for the order. Let H have order at least k, and let the series a i and b i have zero constant coefficient, with a i - b i of order at least n. Then H(a) - H(b) has order at least n + k - 1.

theorem MvPowerSeries.coeff_subst_sub_subst_of_degree_le {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {n : ℕ} [CommRing R] [Fintype σ] (H : MvPowerSeries σ R) {a b : σ → MvPowerSeries τ R} (ha₀ : ∀ (i : σ), constantCoeff (a i) = 0) (hb₀ : ∀ (i : σ), constantCoeff (b i) = 0) (hab : ∀ (i : σ), ↑n ≤ (a i - b i).order) {e : τ →₀ ℕ} (he : Finsupp.degree e ≤ n) : (coeff e) (subst a H - subst b H) = ∑ i : σ, (coeff (Finsupp.single i 1)) H * (coeff e) (a i - b i)

The linear part of a difference of substitutions. If the series a i and b i have zero constant coefficient and a i - b i has order at least n, then in degrees at most n the coefficients of H(a) - H(b) are those of ∑ᵢ hᵢ (a i - b i), where hᵢ is the coefficient of Xᵢ in H.

theorem MvPowerSeries.coeff_mul_eq_coeff_mul_constantCoeff_of_le_order {σ : Type u_1} {R : Type u_2} [Ring R] {e : MvPowerSeries σ R} {n : ℕ} (he : ↑n ≤ e.order) (q : MvPowerSeries σ R) {m : σ →₀ ℕ} (hm : Finsupp.degree m ≤ n) : (coeff m) (e * q) = (coeff m) e * constantCoeff q

Below degree n + 1, multiplying a series e of order at least n by q scales it by the constant coefficient of q.

theorem MvPowerSeries.le_order_subst_update_add_sub {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [DecidableEq σ] (f : MvPowerSeries σ R) {a : σ → MvPowerSeries τ S} (ha : HasSubst a) (ha₀ : ∀ (t : σ), constantCoeff (a t) = 0) (s : σ) {e : MvPowerSeries τ S} {n : ℕ} (hn : n ≠ 0) (he : ↑n ≤ e.order) : ↑(n + 1) ≤ (subst (Function.update a s (a s + e)) f - subst a f - (algebraMap R S) ((coeff (Finsupp.single s 1)) f) • e).order

The lowest-order effect of perturbing a substitution. Let the series a t have zero constant coefficient, and perturb the entry a s by a series e of order at least n ≥ 1. Then f(a) changes by c e, where c is the coefficient of Xₛ in f, up to terms of degree greater than n.

theorem MvPowerSeries.homogeneousComponent_one_eq_X_add_X {R : Type u_1} {f : MvPowerSeries (Fin 2) R} [Semiring R] (hX : (coeff (Finsupp.single 0 1)) f = 1) (hY : (coeff (Finsupp.single 1 1)) f = 1) : (homogeneousComponent 1) f = X 0 + X 1

A series whose two linear coefficients are one has degree-one homogeneous component X + Y, independently of its constant coefficient.

theorem MvPowerSeries.two_le_order_sub_X_add_X {R : Type u_1} {f : MvPowerSeries (Fin 2) R} [Ring R] (h₀ : constantCoeff f = 0) (hX : (coeff (Finsupp.single 0 1)) f = 1) (hY : (coeff (Finsupp.single 1 1)) f = 1) : 2 ≤ (f - (X 0 + X 1)).order

A power series in two variables with zero constant coefficient and linear part X + Y differs from X + Y by a series of order at least two.

theorem MvPowerSeries.homogeneousComponent_one_subst_pair {R : Type u_1} {f : MvPowerSeries (Fin 2) R} {τ : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (h₀ : constantCoeff f = 0) (hX : (coeff (Finsupp.single 0 1)) f = 1) (hY : (coeff (Finsupp.single 1 1)) f = 1) {x y : MvPowerSeries τ S} (hx : constantCoeff x = 0) (hy : constantCoeff y = 0) : (homogeneousComponent 1) (subst ![x, y] f) = (homogeneousComponent 1) x + (homogeneousComponent 1) y

If f has zero constant coefficient and linear part X + Y, the linear part of f(x, y) is the sum of the linear parts of x and y, for x and y without constant coefficient.