Exponents, weights and the Weierstrass polynomial over a commutative ring

Lemmas about exponents, radius vectors and the Weierstrass polynomial over an arbitrary commutative ring that do not depend on the coefficient field: the weight ρ^ν of a monomial under a shift of the distinguished exponent or a scaling of the tail radii; the exponents of series in one variable and the embedding of the distinguished coordinate; the exponents cons k x of a split monomial x_0^k x'^x and their weights; the polynomial weierstrassPolynomial d c = X^d + ∑_{j<d} C(c_j) X^{d-1-j} over a commutative ring, with its coefficients, its monicity and degree and its evaluation; and a common positive lower bound for finitely many radius vectors.

Weights of exponents under the splitting operators and the tail scaling

theorem Analytic.monomialEval_add_single_zero {m : ℕ} (ρ : Fin (m + 1) → NNReal) (ν : Fin (m + 1) →₀ ℕ) (d : ℕ) : monomialEval ρ (ν + Finsupp.single 0 d) = monomialEval ρ ν * ρ 0 ^ d

The weight of x^{ν + d e_0} is ρ_0^d times the weight of x^ν.

theorem Analytic.monomialEval_tailScale_le {m : ℕ} (ρ : Fin (m + 1) → NNReal) {t : NNReal} (ht : t ≤ 1) {ν : Fin (m + 1) →₀ ℕ} {j : Fin (m + 1)} (hj : j ≠ 0) (hν : ν j ≠ 0) : monomialEval (fun (k : Fin (m + 1)) => if k = 0 then ρ 0 else t * ρ k) ν ≤ t * monomialEval ρ ν

Shrinking the tail radii by t ≤ 1 multiplies the weight of a monomial containing a tail variable x_j by at most t.

theorem Analytic.eq_single_zero_of_tail_eq_zero {m : ℕ} {ν : Fin (m + 1) →₀ ℕ} (hν : ∀ (j : Fin (m + 1)), j ≠ 0 → ν j = 0) : ν = Finsupp.single 0 (ν 0)

A monomial exponent with no tail variable is a pure x_0-power.

Exponents in one variable and the distinguished coordinate

theorem Analytic.Fin1.eq_single (ν : Fin 1 →₀ ℕ) : ν = Finsupp.single 0 (ν 0)

An exponent in one variable is a pure power.

theorem Analytic.Fin1.eq_zero_iff (ν : Fin 1 →₀ ℕ) : ν = 0 ↔ ν 0 = 0

theorem Analytic.Fin1.single_apply_injective {m : ℕ} : Function.Injective fun (ν : Fin 1 →₀ ℕ) => Finsupp.single 0 (ν 0)

theorem Analytic.monomialEval_fin1 {R : Type u_1} [CommMonoid R] (y : Fin 1 → R) (ν : Fin 1 →₀ ℕ) : monomialEval y ν = y 0 ^ ν 0

def Analytic.embFirst (m : ℕ) : Fin 1 ↪ Fin (m + 1)

The embedding of the single variable onto the distinguished coordinate.

Equations

• Analytic.embFirst m = { toFun := fun (x : Fin 1) => 0, inj' := ⋯ }

Split exponents cons k x and the Weierstrass polynomial over a commutative ring

theorem Analytic.cons_zero_eq_single {m : ℕ} (k : ℕ) : Finsupp.cons k 0 = Finsupp.single 0 k

theorem Analytic.cons_eq_cons_iff {m k k' : ℕ} {x x' : Fin m →₀ ℕ} : Finsupp.cons k x = Finsupp.cons k' x' ↔ k = k' ∧ x = x'

theorem Analytic.degree_cons {m : ℕ} (k : ℕ) (x : Fin m →₀ ℕ) : Finsupp.degree (Finsupp.cons k x) = k + Finsupp.degree x

theorem Analytic.embDomain_succEmb {m : ℕ} (x : Fin m →₀ ℕ) : Finsupp.embDomain (Fin.succEmb m) x = Finsupp.cons 0 x

theorem Analytic.cons_sub_single_zero {m : ℕ} (k n : ℕ) (x : Fin m →₀ ℕ) : Finsupp.cons k x - Finsupp.single 0 n = Finsupp.cons (k - n) x

noncomputable def Analytic.weierstrassPolynomial {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) : Polynomial R

The Weierstrass polynomial X^d + ∑_{j<d} C(c_j) X^{d-1-j} over a commutative ring R (used over the tail ring of power series and, pointwise, over the coefficient field).

Equations

• Analytic.weierstrassPolynomial d c = Polynomial.X ^ d + ∑ j : Fin d, Polynomial.C (c j) * Polynomial.X ^ (d - 1 - ↑j)

theorem Analytic.coeff_weierstrassPolynomial_of_lt {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) {n : ℕ} (hn : n < d) : (weierstrassPolynomial d c).coeff n = c ⟨d - 1 - n, ⋯⟩

theorem Analytic.coeff_weierstrassPolynomial_rev {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) (j : Fin d) : (weierstrassPolynomial d c).coeff (d - 1 - ↑j) = c j

theorem Analytic.coeff_weierstrassPolynomial_self {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) : (weierstrassPolynomial d c).coeff d = 1

theorem Analytic.coeff_weierstrassPolynomial_of_gt {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) {n : ℕ} (hn : d < n) : (weierstrassPolynomial d c).coeff n = 0

theorem Analytic.degree_weierstrassPolynomial_sum_lt {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) : (∑ j : Fin d, Polynomial.C (c j) * Polynomial.X ^ (d - 1 - ↑j)).degree < ↑d

theorem Analytic.monic_weierstrassPolynomial {R : Type u_1} [CommRing R] [Nontrivial R] (d : ℕ) (c : Fin d → R) : (weierstrassPolynomial d c).Monic

theorem Analytic.natDegree_weierstrassPolynomial {R : Type u_1} [CommRing R] [Nontrivial R] (d : ℕ) (c : Fin d → R) : (weierstrassPolynomial d c).natDegree = d

theorem Analytic.eval_weierstrassPolynomial {R : Type u_1} [CommRing R] (d : ℕ) (c : Fin d → R) (t : R) : Polynomial.eval t (weierstrassPolynomial d c) = t ^ d + ∑ j : Fin d, c j * t ^ (d - 1 - ↑j)

Weights of split exponents

theorem Analytic.cons_injective {m : ℕ} (k : ℕ) : Function.Injective fun (x : Fin m →₀ ℕ) => Finsupp.cons k x

A common radius vector

theorem Analytic.Radius.exists_le_forall {m : ℕ} {ι : Type u_1} [Finite ι] (s : ι → Radius m) : ∃ (ρ : Radius m), ∀ (i : ι) (k : Fin m), ↑ρ k ≤ ↑(s i) k

A finite family of radius vectors has a common positive lower bound.