Polynomial

Results named in Tau Ceti's TauCeti.Analysis.Polynomial modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCauchy's bound on the symmetric power#

the points of an unordered tuple are bounded by one more than the sup-norm of its elementary symmetric chart, because each of them is a root of the monic polynomial those coordinates present.

TauCeti.Sym.norm_le_norm_coeffEquiv_ofFn_add_one.{u_1} {K : Type u_1} [NormedField K]
  [IsAlgClosed K] {n : ℕ} (f : Fin n → K) :
  ‖f‖ ≤ ‖(TauCeti.Sym.coeffEquiv K n) (TauCeti.Sym.ofFn f)‖ + 1
Lean

Formalized in Tau Ceti as TauCeti.Sym.norm_le_norm_coeffEquiv_ofFn_add_one.

Sources
LeanTauCeti.Sym.norm_le_norm_coeffEquiv_ofFn_add_one
Used by 3
Used byThe symmetric power of a complex curve is a complex analytic manifold · Existence of adapted cylindrical algebraic decompositions · The local Nash graph criterion

TheoremColeman's bound for truncations#

Let ρ be a nonnegative antitone Newton majorant of a power series F, ‖coeff j F‖ ≤ ∏ i < j, ρ i, and let B be restricted at every radius ρ i with B(0) = 0. Then the Coleman transforms of the truncations of F along the truncations of B satisfy ‖coeff k D_(n,m)(trunc a B, trunc b F)‖ ≤ ∏ i < k, β_B(ρ i), uniformly in the ranks, degree bounds and truncation orders. In particular this bounds D_(N,M)(trunc (M + 1) B, trunc (N + 1) F).

PowerSeries.norm_coeff_colemanDBounded_trunc_le.{u_1} {R : Type u_1} [NormedCommRing R]
  [NormOneClass R] [IsUltrametricDist R] {F B : PowerSeries R} {ρ : ℕ → ℝ}
  (hρ₀ : ∀ (i : ℕ), 0 ≤ ρ i) (hρ : Antitone ρ)
  (hF : ∀ (j : ℕ), ‖(PowerSeries.coeff j) F‖ ≤ ∏ i ∈ Finset.range j, ρ i)
  (hB : ∀ (i : ℕ), PowerSeries.IsRestricted (ρ i) B) (hB₀ : (PowerSeries.coeff 0) B = 0)
  (n m a b k : ℕ) :
  ‖(((PowerSeries.trunc a) B).colemanDBounded ((PowerSeries.trunc b) F) n m).coeff k‖ ≤
    ∏ i ∈ Finset.range k, B.colemanMajorant (ρ i)
Lean

Formalized in Tau Ceti as PowerSeries.norm_coeff_colemanDBounded_trunc_le.

Sources
LeanPowerSeries.norm_coeff_colemanDBounded_trunc_le
Uses 1
Proof usesColeman's coefficient bound

TheoremColeman's coefficient bound#

Let P and B be polynomials over an ultrametric seminormed ring with ‖1‖ = 1 and B(0) = 0. If ρ is a nonnegative antitone sequence with ‖coeff j P‖ ≤ ∏ i < j, ρ i for j ≤ n, and ‖coeff l B‖ * ρ t ^ l ≤ β t for every t and every l ≥ 1, then the k-th coefficient of Coleman's transform D_(n,m)(B, P) has norm at most ∏ t < k, β t, for all ranks n and degree bounds m.

Polynomial.norm_coeff_colemanDBounded_le.{u_1} {R : Type u_1} [SeminormedCommRing R]
  {B P : Polynomial R} {n m : ℕ} [NormOneClass R] [IsUltrametricDist R] {ρ β : ℕ → ℝ}
  (hB₀ : B.coeff 0 = 0) (hρ₀ : ∀ (i : ℕ), 0 ≤ ρ i) (hρ : Antitone ρ)
  (hP : ∀ j ≤ n, ‖P.coeff j‖ ≤ ∏ i ∈ Finset.range j, ρ i)
  (hβ : ∀ (t j : ℕ), ‖B.coeff (j + 1)‖ * ρ t ^ (j + 1) ≤ β t) (k : ℕ) :
  ‖(B.colemanDBounded P n m).coeff k‖ ≤ ∏ t ∈ Finset.range k, β t
Lean

Formalized in Tau Ceti as Polynomial.norm_coeff_colemanDBounded_le.

Sources
LeanPolynomial.norm_coeff_colemanDBounded_le
Used by 2
Used byColeman's bound for truncations · Coleman's perturbation bound

TheoremColeman's perturbation bound#

Let ρ be a nonnegative antitone sequence and r ≥ 1. If P₁ has Newton majorant ρ up to degree n, the perturbation P₂ - P₁ satisfies the same bound after multiplication by r, and the coefficients of positive degree of B₁ and of r (B₂ - B₁) are bounded by β at every radius ρ t, where B₁(0) = B₂(0) = 0, then the coefficients of the bounded Coleman transforms satisfy dist (coeff k D_(n,m)(B₂, P₂)) (coeff k D_(n,m)(B₁, P₁)) * r ≤ ∏ t < k, β t.

Thus perturbing the inputs by a factor r⁻¹ relative to their majorants moves every coefficient of the transform by at most r⁻¹ times its coefficient bound Polynomial.norm_coeff_colemanDBounded_le, uniformly in the ranks n and degree bounds m.

Polynomial.dist_coeff_colemanDBounded_mul_le.{u_1} {R : Type u_1} [NormedCommRing R]
  [NormOneClass R] [IsUltrametricDist R] {B₁ B₂ P₁ P₂ : Polynomial R} {n m : ℕ} {ρ β : ℕ → ℝ}
  {r : ℝ} (hB₁ : B₁.coeff 0 = 0) (hB₂ : B₂.coeff 0 = 0) (hρ₀ : ∀ (i : ℕ), 0 ≤ ρ i) (hρ : Antitone ρ)
  (hr : 1 ≤ r) (hP₁ : ∀ j ≤ n, ‖P₁.coeff j‖ ≤ ∏ i ∈ Finset.range j, ρ i)
  (hP : ∀ j ≤ n, ‖(P₂ - P₁).coeff j‖ * r ≤ ∏ i ∈ Finset.range j, ρ i)
  (hβ₁ : ∀ (t j : ℕ), ‖B₁.coeff (j + 1)‖ * ρ t ^ (j + 1) ≤ β t)
  (hβ : ∀ (t j : ℕ), ‖(B₂ - B₁).coeff (j + 1)‖ * r * ρ t ^ (j + 1) ≤ β t) (k : ℕ) :
  dist ((B₂.colemanDBounded P₂ n m).coeff k) ((B₁.colemanDBounded P₁ n m).coeff k) * r ≤
    ∏ t ∈ Finset.range k, β t
Lean

Formalized in Tau Ceti as Polynomial.dist_coeff_colemanDBounded_mul_le.

Sources
LeanPolynomial.dist_coeff_colemanDBounded_mul_le
Uses 1
Proof usesColeman's coefficient bound

TheoremNorthcott's theorem for integer polynomials#

Only finitely many integer polynomials have degree at most n and coefficient sup norm (naive height) at most B.

Polynomial.finite_setOf_natDegree_le_supNorm_le (n : ℕ) (B : ℝ) :
  {P | P.natDegree ≤ n ∧ P.supNorm ≤ B}.Finite
Lean

Formalized in Tau Ceti as Polynomial.finite_setOf_natDegree_le_supNorm_le.

Sources
LeanPolynomial.finite_setOf_natDegree_le_supNorm_le

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.