Documentation

TauCeti.Analysis.Polynomial.Ultra

Polynomial bounds over ultrametric rings #

Over an ultrametric seminormed commutative ring with ‖1‖ = 1, let p a be polynomials of degree at most one whose constant coefficients have norm at most one and whose linear coefficients have norm at most r a. The m-th coefficient of ∏ a ∈ s, p a is a sum of products of m linear and #s - m constant coefficients, so the ultrametric inequality bounds it by every common bound for the products ∏ a ∈ t, r a over the m-element subsets t of s (TauCeti.norm_coeff_prod_le_of_natDegree_le_one). Applied to the Leibniz expansion, this bounds the coefficients of determinants such as det (1 - X A) and of the adjugate of 1 - X A.

An integral polynomial has norm at most one on the closed unit ball of an ultrametric seminormed ring with ‖1‖ = 1 (Polynomial.norm_aeval_le_one).

References #

An integral polynomial evaluated at a point of the closed unit ball of a non-archimedean seminormed ring with ‖1‖ = 1 has norm at most one.

theorem TauCeti.norm_coeff_prod_le_of_natDegree_le_one {α : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {s : Finset α} {p : α → Polynomial R} {r : α → ℝ} (hdeg : ∀ a ∈ s, (p a).natDegree ≤ 1) (h₀ : ∀ a ∈ s, ‖(p a).coeff 0‖ ≤ 1) (h₁ : ∀ a ∈ s, ‖(p a).coeff 1‖ ≤ r a) {m : ℕ} {c : ℝ} (hc : 0 ≤ c) (hs : ∀ t ⊆ s, t.card = m → ∏ a ∈ t, r a ≤ c) :
‖(∏ a ∈ s, p a).coeff m‖ ≤ c

Coefficients of a product of linear polynomials. Over an ultrametric seminormed commutative ring with ‖1‖ = 1, let p a be polynomials of degree at most one with ‖(p a).coeff 0‖ ≤ 1 and ‖(p a).coeff 1‖ ≤ r a. If c ≥ 0 bounds ∏ a ∈ t, r a for every m-element subset t of s, then c bounds the m-th coefficient of ∏ a ∈ s, p a.