Rescaling multivariate power series

This file records general facts about Mathlib's coefficientwise rescaling of multivariate power series. If scalars uᵢ scale norms in a module by rᵢ / sᵢ, then the monomial uᵗ turns weighted norms at s into weighted norms at r. Hence rescaling by multiplicative units transports weighted coefficient norms, and restrictedness, when the weights are changed by the corresponding scalar norms; in particular, rescaling by the inverses of multiplicative units uᵢ turns the weighted coefficient norms at the radii ‖uᵢ‖⁻¹ into plain coefficient norms. Rescaling by a family of units and then by their inverses is the identity. Substituting a family into a rescaled power series is substituting the rescaled family: f(a X) at X = v is f(a v); in particular, s • g = f(s X) gives s • g(v) = f(s v).

theorem TauCeti.MvPowerSeries.norm_prod_pow_smul_mul_prod {σ : Type u_1} {R : Type u_2} {E : Type u_3} [SeminormedCommRing R] [SeminormedAddCommGroup E] [Module R E] {r s : σ → ℝ} (u : σ → R) (hu : ∀ (i : σ) (e : E), ‖u i • e‖ * s i = ‖e‖ * r i) (t : σ →₀ ℕ) (e : E) : (‖(t.prod fun (i : σ) (m : ℕ) => u i ^ m) • e‖ * t.prod fun (x1 : σ) (x2 : ℕ) => s x1 ^ x2) = ‖e‖ * t.prod fun (x1 : σ) (x2 : ℕ) => r x1 ^ x2

If each u i scales norms in E by r i / s i, then the monomial uᵗ scales the weighted coefficient norms: ‖uᵗ • e‖ * sᵗ = ‖e‖ * rᵗ.

theorem TauCeti.MvPowerSeries.norm_smul_mul_of_isNormMulUnit {σ : Type u_1} {R : Type u_2} [SeminormedCommRing R] {r s : σ → ℝ} (u : σ → R) (hu : ∀ (i : σ), IsNormMulUnit (u i)) (hrs : ∀ (i : σ), ‖u i‖ * s i = r i) (i : σ) (e : R) : ‖u i • e‖ * s i = ‖e‖ * r i

Multiplicative units u i with ‖u i‖ * s i = r i scale norms in R by r i / s i, which is the scaling hypothesis of norm_prod_pow_smul_mul_prod for E = R.

theorem MvPowerSeries.norm_coeff_rescale_mul_prod {σ : Type u_1} {R : Type u_2} [NormedCommRing R] {r s : σ → ℝ} (u : σ → R) (hu : ∀ (i : σ), TauCeti.IsNormMulUnit (u i)) (hrs : ∀ (i : σ), ‖u i‖ * s i = r i) (f : MvPowerSeries σ R) (n : σ →₀ ℕ) : (‖(coeff n) ((rescale u) f)‖ * n.prod fun (x1 : σ) (x2 : ℕ) => s x1 ^ x2) = ‖(coeff n) f‖ * n.prod fun (x1 : σ) (x2 : ℕ) => r x1 ^ x2

Rescaling by multiplicative units preserves weighted coefficient norms when the weights are changed by the corresponding scalar norms.

theorem MvPowerSeries.isRestricted_rescale_iff {σ : Type u_1} {R : Type u_2} [NormedCommRing R] {r s : σ → ℝ} (u : σ → R) (hu : ∀ (i : σ), TauCeti.IsNormMulUnit (u i)) (hrs : ∀ (i : σ), ‖u i‖ * s i = r i) (f : MvPowerSeries σ R) : IsRestricted s ((rescale u) f) ↔ IsRestricted r f

Rescaling by multiplicative units converts restrictedness at r into restrictedness at s when ‖u i‖ * s i = r i.

theorem MvPowerSeries.norm_coeff_rescale_units_inv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] {r : σ → ℝ} (u : σ → Rˣ) (hu : ∀ (i : σ), TauCeti.IsNormMulUnit ↑(u i)) (hr : ∀ (i : σ), ‖↑(u i)‖ * r i = 1) (f : MvPowerSeries σ R) (n : σ →₀ ℕ) : ‖(coeff n) ((rescale fun (i : σ) => ↑(u i)⁻¹) f)‖ = ‖(coeff n) f‖ * n.prod fun (x1 : σ) (x2 : ℕ) => r x1 ^ x2

Weight bounds from multiplicative units. If each u i is a multiplicative unit and ‖u i‖ * r i = 1, then rescaling by the inverse units turns the weighted coefficient norms at the radii r into plain coefficient norms: the coefficient of f(u⁻¹ X) at n has norm ‖coeff n f‖ * rⁿ.

theorem MvPowerSeries.rescale_inv_rescale {σ : Type u_1} {A : Type u_3} [CommSemiring A] (u : σ → Aˣ) (f : MvPowerSeries σ A) : (rescale fun (i : σ) => ↑(u i)⁻¹) ((rescale fun (i : σ) => ↑(u i)) f) = f

Rescaling by a family of units and then by their inverses is the identity.

theorem MvPowerSeries.subst_rescale {σ : Type u_1} {τ : Type u_3} {A : Type u_4} [CommRing A] (a : σ → A) (f : MvPowerSeries σ A) {v : σ → MvPowerSeries τ A} (hv : HasSubst v) : subst v ((rescale a) f) = subst (a • v) f

Substituting a family v into the rescaling f(a X) of f substitutes the rescaled family: f(a X) at X = v is f(a v).

theorem MvPowerSeries.smul_subst_of_smul_eq_rescale {σ : Type u_1} {τ : Type u_3} {A : Type u_4} [CommRing A] {f g : MvPowerSeries σ A} {s : A} (h : s • g = (rescale fun (x : σ) => s) f) {v : σ → MvPowerSeries τ A} (hv : HasSubst v) : s • subst v g = subst (s • v) f

If s • g = f(s X), then s • g(v) = f(s v) at every substitutable family v.