Expanding multivariate power series

This file records general facts about Mathlib's expansion f(X) ↦ f(X^p) of multivariate power series. Substituting X i ↦ X i ^ p multiplies every exponent by p, so the weight of p • μ at the polyradii r is the weight of μ at r ^ p, and f(X^p) is restricted at r exactly when f is restricted at r ^ p. In finitely many variables, the coefficient at p • μ + ν of a sum ∑ X^ν' g_ν'(X^p) over the exponents ν' with ν' i < p is the coefficient at μ of g_ν; this is the formal uniqueness of the decomposition along the expansion.

Expansion by p ^ i is the integral shadow of the Frobenius: if φ is a ring endomorphism with φ(a) ≡ a ^ (p ^ i) modulo p, then ψ ^ (p ^ i) ≡ (φ ψ)(X ^ (p ^ i)) modulo p for every power series ψ, where φ ψ applies φ to the coefficients. Modulo p this is Mathlib's MvPowerSeries.map_iterateFrobenius_expand. Such congruences drive integrality arguments for power series defined by functional equations, as in Hazewinkel's functional equation lemma.

Main results

• MvPowerSeries.prod_pow_nsmul: the weight of p • μ at r is the weight of μ at r ^ p.
• MvPowerSeries.isRestricted_expand_iff: f(X^p) is restricted at r exactly when f is restricted at r ^ p.
• MvPowerSeries.IsRestricted.coeff_nsmul_add: restrictedness of an expansion component.
• MvPowerSeries.coeff_sum_monomial_mul_expand: the coefficients of ∑ X^ν g_ν(X^p).
• MvPowerSeries.natCast_dvd_pow_sub_expand_map: if φ(a) ≡ a ^ (p ^ i) modulo the prime p, then p divides ψ ^ (p ^ i) - (φ ψ)(X ^ (p ^ i)).

theorem MvPowerSeries.prod_pow_nsmul {σ : Type u_1} (p : ℕ) {M : Type u_2} [CommMonoid M] {r t : σ → M} (ht : ∀ (i : σ), r i ^ p = t i) (μ : σ →₀ ℕ) : ((p • μ).prod fun (x1 : σ) (x2 : ℕ) => r x1 ^ x2) = μ.prod fun (x1 : σ) (x2 : ℕ) => t x1 ^ x2

The weight at the polyradii r of the exponent p • μ is the weight of μ at the polyradii t = r ^ p.

theorem MvPowerSeries.isRestricted_expand_iff {σ : Type u_1} (p : ℕ) (hp : p ≠ 0) {R : Type u_2} [NormedCommRing R] {r t : σ → ℝ} (ht : ∀ (i : σ), r i ^ p = t i) {f : MvPowerSeries σ R} : IsRestricted r ((expand p hp) f) ↔ IsRestricted t f

Restrictedness of an expansion. The series f(X^p) is restricted at the polyradii r exactly when f is restricted at the polyradii r ^ p.

theorem MvPowerSeries.IsRestricted.coeff_nsmul_add {σ : Type u_1} {R : Type u_2} [NormedRing R] {r t : σ → ℝ} [∀ (i : σ), Fact (0 < r i)] {p : ℕ} {f : MvPowerSeries σ R} (hf : IsRestricted r f) (hp : p ≠ 0) (ht : ∀ (i : σ), r i ^ p = t i) (ν : σ →₀ ℕ) : IsRestricted t fun (μ : σ →₀ ℕ) => (coeff (p • μ + ν)) f

Extracting the coefficients in an arithmetic progression of exponents preserves restrictedness, with the polyradii raised to the common step.

theorem MvPowerSeries.coeff_sum_monomial_mul_expand {σ : Type u_1} (p : ℕ) (hp : p ≠ 0) {R : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (g : (σ → Fin p) → MvPowerSeries σ R) (μ : σ →₀ ℕ) (ν : σ → Fin p) : (coeff (p • μ + Finsupp.equivFunOnFinite.symm (Fin.val ∘ ν))) (∑ ν' : σ → Fin p, (monomial (Finsupp.equivFunOnFinite.symm (Fin.val ∘ ν'))) 1 * (expand p hp) (g ν')) = (coeff μ) (g ν)

The coefficient at p • μ + ν of a sum ∑ X^ν' g_ν'(X^p) over the exponents ν' with ν' i < p is the coefficient at μ of g_ν.

theorem MvPowerSeries.natCast_dvd_pow_sub_expand_map {σ : Type u_1} {A : Type u_2} [CommRing A] {p : ℕ} [Fact (Nat.Prime p)] (i : ℕ) {φ : A →+* A} (hφ : ∀ (a : A), ↑p ∣ φ a - a ^ p ^ i) (ψ : MvPowerSeries σ A) : ↑p ∣ ψ ^ p ^ i - (expand (p ^ i) ⋯) ((map φ) ψ)

The Frobenius congruence for power series. Let p be a prime and φ a ring endomorphism of A with φ(a) ≡ a ^ (p ^ i) modulo p for all a. Then p divides ψ ^ (p ^ i) - (φ ψ)(X ^ (p ^ i)) for every power series ψ over A, where φ ψ applies φ to the coefficients of ψ.