Substitution and products of expanded power series

For a family of power series f c and positive multipliers m c, this file computes the coefficients of the product ∏ c, f c (X ^ m c) of the expanded series PowerSeries.expand (m c) _ (f c). The n-th coefficient of a finite product is a sum over the weighted antidiagonal Finset.weightedFinsuppAntidiag s m n of the assignments l supported in s with ∑ c ∈ s, m c * l c = n. When every f c has constant term 1, factors with n < m c do not change the n-th coefficient. So if only finitely many m c lie below each bound, the infinite product converges in the coefficientwise topology (PowerSeries.WithPiTopology), and each coefficient is that of a finite product. Over a finite field with q elements, the iterates of expand q are the q ^ j-th power maps.

Main declarations

• PowerSeries.expand_injective: expansion f ↦ f (X ^ p) is injective.
• PowerSeries.rescale_expand: rescaling f (X ^ p) by a rescales f by a ^ p.
• PowerSeries.subst_expand: substituting into f(X ^ p) substitutes the p-th power.
• PowerSeries.toMvPowerSeries_expand: embedding in one coordinate commutes with expansion.
• Finset.weightedFinsuppAntidiag s m n: the assignments l : ι →₀ ℕ supported in s with ∑ c ∈ s, m c * l c = n.
• PowerSeries.coeff_prod_expand: the n-th coefficient of ∏ c ∈ s, f c (X ^ m c) is the sum over l ∈ s.weightedFinsuppAntidiag m n of ∏ c ∈ s, coeff (l c) (f c).
• PowerSeries.coeff_prod_expand_of_subset: adjoining factors with n < m c and constant term 1 does not change the n-th coefficient.
• PowerSeries.X_pow_dvd_expand_sub_C_constantCoeff: an expanded series agrees with its constant coefficient modulo the corresponding power of X.
• PowerSeries.hasProd_expand, PowerSeries.multipliable_expand, PowerSeries.coeff_tprod_expand: the infinite product of the expanded series and its coefficients, when {c | m c ≤ n} is finite for every n.
• FiniteField.PowerSeries.expand_card_pow_apply: over a finite field K with q elements, the j-th iterate of expand q is the q ^ j-th power map.

noncomputable def Finset.weightedFinsuppAntidiag {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (n : ℕ) : Finset (ι →₀ ℕ)

The weighted antidiagonal: the assignments l : ι →₀ ℕ supported in s with ∑ c ∈ s, m c * l c = n.

@[simp]

theorem Finset.mem_weightedFinsuppAntidiag {ι : Type u_1} {s : Finset ι} {m : ι → ℕ+} {n : ℕ} {l : ι →₀ ℕ} : l ∈ s.weightedFinsuppAntidiag m n ↔ l.support ⊆ s ∧ ∑ c ∈ s, ↑(m c) * l c = n

An assignment lies in the weighted antidiagonal exactly when it is supported in s and has weighted sum n.

theorem Finset.mul_le_of_mem_weightedFinsuppAntidiag {ι : Type u_1} {s : Finset ι} {m : ι → ℕ+} {n : ℕ} {l : ι →₀ ℕ} (hl : l ∈ s.weightedFinsuppAntidiag m n) (c : ι) : ↑(m c) * l c ≤ n

Every summand m c * l c of an element l of the weighted antidiagonal is at most n.

theorem PowerSeries.order_eq_of_order_expand_eq {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) {f : PowerSeries R} {n : ℕ} (hf : ((expand p hp) f).order = ↑(p * n)) : f.order = ↑n

Recover the finite order of a series from the order of its expansion.

theorem PowerSeries.expand_injective {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) : Function.Injective ⇑(expand p hp)

Expansion f ↦ f (X ^ p) is injective: the coefficients of f reappear as the coefficients of f (X ^ p) in degrees divisible by p.

theorem PowerSeries.rescale_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (a : R) (f : PowerSeries R) : (rescale a) ((expand p hp) f) = (expand p hp) ((rescale (a ^ p)) f)

Rescaling an expanded series by a is expanding the series rescaled by a ^ p: f ((a X) ^ p) = (f (a ^ p X)) (X ^ p).

theorem PowerSeries.subst_expand {R : Type u_2} [CommRing R] {σ : Type u_3} (p : ℕ) (hp : p ≠ 0) {a : MvPowerSeries σ R} (ha : HasSubst a) (f : PowerSeries R) : subst a ((expand p hp) f) = subst (a ^ p) f

Substituting into an expanded series raises the substituted series to the expansion power.

theorem PowerSeries.toMvPowerSeries_expand {R : Type u_2} [CommRing R] {σ : Type u_3} (p : ℕ) (hp : p ≠ 0) (i : σ) (f : PowerSeries R) : (toMvPowerSeries i) ((expand p hp) f) = (MvPowerSeries.expand p hp) ((toMvPowerSeries i) f)

Embedding a series in one coordinate commutes with expansion.

theorem PowerSeries.coeff_prod_expand {ι : Type u_1} {R : Type u_2} [CommRing R] (s : Finset ι) (m : ι → ℕ+) (f : ι → PowerSeries R) (n : ℕ) : (coeff n) (∏ c ∈ s, (expand ↑(m c) ⋯) (f c)) = ∑ l ∈ s.weightedFinsuppAntidiag m n, ∏ c ∈ s, (coeff (l c)) (f c)

Expansion of a product of expanded power series: the n-th coefficient of ∏ c ∈ s, f c (X ^ m c) is the sum, over all l ∈ s.weightedFinsuppAntidiag m n, of the products ∏ c ∈ s, coeff (l c) (f c).

theorem PowerSeries.coeff_prod_expand_of_subset {ι : Type u_1} {R : Type u_2} [CommRing R] {s t : Finset ι} (hst : s ⊆ t) {m : ι → ℕ+} {f : ι → PowerSeries R} {n : ℕ} (h : ∀ c ∈ t, c ∉ s → n < ↑(m c)) (hf : ∀ c ∈ t, c ∉ s → constantCoeff (f c) = 1) : (coeff n) (∏ c ∈ t, (expand ↑(m c) ⋯) (f c)) = (coeff n) (∏ c ∈ s, (expand ↑(m c) ⋯) (f c))

Finite cutoff for a product of expanded power series: adjoining factors f c (X ^ m c) with n < m c and constant term 1 does not change the n-th coefficient.

theorem PowerSeries.X_pow_dvd_expand_sub_C_constantCoeff {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (f : PowerSeries R) : X ^ p ∣ (expand p hp) f - C (constantCoeff f)

An expanded series f (X ^ p) agrees with its constant coefficient modulo X ^ p.

theorem PowerSeries.hasProd_expand {ι : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] {m : ι → ℕ+} (hm : ∀ (n : ℕ), {c : ι | ↑(m c) ≤ n}.Finite) {f : ι → PowerSeries R} (hf : ∀ (c : ι), constantCoeff (f c) = 1) : HasProd (fun (c : ι) => (expand ↑(m c) ⋯) (f c)) (mk fun (n : ℕ) => (coeff n) (∏ c ∈ ⋯.toFinset, (expand ↑(m c) ⋯) (f c)))

If {c | m c ≤ n} is finite for every n and every f c has constant term 1, the finite products of the factors f c (X ^ m c) converge in the coefficientwise topology (PowerSeries.WithPiTopology), the n-th coefficient of the limit being that of the product over {c | m c ≤ n}.

theorem PowerSeries.multipliable_expand {ι : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] {m : ι → ℕ+} (hm : ∀ (n : ℕ), {c : ι | ↑(m c) ≤ n}.Finite) {f : ι → PowerSeries R} (hf : ∀ (c : ι), constantCoeff (f c) = 1) : Multipliable fun (c : ι) => (expand ↑(m c) ⋯) (f c)

If {c | m c ≤ n} is finite for every n and every f c has constant term 1, the factors f c (X ^ m c) have an infinite product in the coefficientwise topology (PowerSeries.WithPiTopology) on R⟦X⟧.

theorem PowerSeries.coeff_tprod_expand {ι : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] [T2Space R] {m : ι → ℕ+} (hm : ∀ (n : ℕ), {c : ι | ↑(m c) ≤ n}.Finite) {f : ι → PowerSeries R} (hf : ∀ (c : ι), constantCoeff (f c) = 1) {s : Finset ι} {n : ℕ} (hs : ∀ (c : ι), ↑(m c) ≤ n → c ∈ s) : (coeff n) (∏' (c : ι), (expand ↑(m c) ⋯) (f c)) = (coeff n) (∏ c ∈ s, (expand ↑(m c) ⋯) (f c))

If {c | m c ≤ n} is finite for every n and every f c has constant term 1, the n-th coefficient of the infinite product ∏' c, f c (X ^ m c) is that of the finite product over any s containing every c with m c ≤ n.

theorem FiniteField.PowerSeries.expand_card_pow_apply {K : Type u_3} [Field K] [Fintype K] (j : ℕ) (F : PowerSeries K) : (PowerSeries.expand (Fintype.card K) ⋯ ^ j) F = F ^ Fintype.card K ^ j

Over a finite field K with q elements, the j-th iterate of expand q is the q ^ j-th power map.