Continuity of polynomial families

For a family of polynomials f x over a topological semiring, indexed by a parameter x, the coefficients of a product are finite sums of products of coefficients of the factors. Hence if every coefficient of each factor is continuous at a point, so is every coefficient of the product. This is used to treat the product of a finite family of polynomials with continuous coefficients as a single polynomial family.

If the degrees of the family are bounded and its coefficients are continuous, then the evaluation (x, t) ↦ (f x).eval t is jointly continuous, since it is a finite sum of products of coefficients with powers of t. The basic example of a family with continuous coefficients is the monic polynomial TauCeti.Polynomial.monicOfCoeff a as a function of its coefficient tuple a.

Main results

• Polynomial.continuousAt_eval: evaluation along a continuous point for a family of locally bounded degree.
• Polynomial.continuousAt_coeff_mul: coefficients of a product of two families.
• Polynomial.continuousAt_coeff_prod: coefficients of a finite product of families.
• Polynomial.continuous_eval_of_continuous_coeff: joint continuity of the evaluation of a family of bounded degree.
• Polynomial.continuous_evalEval: joint continuity of bivariate polynomial evaluation.
• Polynomial.tendsto_resultant: continuity of the resultant at fixed formal degrees in the coefficients of its arguments.
• TauCeti.Polynomial.continuous_coeff_monicOfCoeff: the coefficients of monicOfCoeff a are continuous in a.
• TauCeti.Polynomial.continuous_coeff_prod_X_sub_C: the coefficients of ∏ i ∈ s, (X - C (f i)) are continuous in the tuple of roots f.

theorem Polynomial.continuous_evalEval {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (P : Polynomial (Polynomial R)) : Continuous fun (z : R × R) => evalEval z.1 z.2 P

Evaluation of a bivariate polynomial is jointly continuous in its two arguments.

theorem Polynomial.continuousAt_eval {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] {f : X → Polynomial R} {r : X → R} {x₀ : X} {d : ℕ} (hf : ∀ i ≤ d, ContinuousAt (fun (x : X) => (f x).coeff i) x₀) (hd : ∀ᶠ (x : X) in nhds x₀, (f x).natDegree ≤ d) (hr : ContinuousAt r x₀) : ContinuousAt (fun (x : X) => eval (r x) (f x)) x₀

Evaluation along a point continuous at x₀ is continuous at x₀ if the coefficients of index at most d are continuous there and the family has degree bounded by d nearby.

theorem Polynomial.continuousAt_coeff_mul {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [TopologicalSpace R] {x₀ : X} [Semiring R] [IsTopologicalSemiring R] {f g : X → Polynomial R} {i : ℕ} (hf : ∀ j ≤ i, ContinuousAt (fun (x : X) => (f x).coeff j) x₀) (hg : ∀ j ≤ i, ContinuousAt (fun (x : X) => (g x).coeff j) x₀) : ContinuousAt (fun (x : X) => (f x * g x).coeff i) x₀

The coefficient of index i in a product of two polynomial families is continuous at x₀ if the coefficients of indices at most i in both factors are continuous there.

theorem Polynomial.continuousAt_coeff_prod {X : Type u_1} {R : Type u_2} {ι : Type u_3} [TopologicalSpace X] [TopologicalSpace R] {x₀ : X} [CommSemiring R] [IsTopologicalSemiring R] {f : ι → X → Polynomial R} (s : Finset ι) {i : ℕ} (hf : ∀ k ∈ s, ∀ j ≤ i, ContinuousAt (fun (x : X) => (f k x).coeff j) x₀) : ContinuousAt (fun (x : X) => (∏ k ∈ s, f k x).coeff i) x₀

The coefficient of index i in a finite product of polynomial families is continuous at x₀ if the coefficients of indices at most i in every factor are continuous there.

theorem Polynomial.continuous_eval_of_continuous_coeff {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] {f : X → Polynomial R} {d : ℕ} (hf : ∀ i ≤ d, Continuous fun (x : X) => (f x).coeff i) (hd : ∀ (x : X), (f x).natDegree ≤ d) : Continuous fun (z : X × R) => eval z.2 (f z.1)

If a family of polynomials has degree at most d and its coefficients of index at most d are continuous, then its evaluation is jointly continuous in the parameter and the point.

theorem Polynomial.tendsto_resultant {R : Type u_2} {ι : Type u_3} [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] {l : Filter ι} {f g : ι → Polynomial R} {f₀ g₀ : Polynomial R} {m n : ℕ} (hf : ∀ k ≤ m, Filter.Tendsto (fun (i : ι) => (f i).coeff k) l (nhds (f₀.coeff k))) (hg : ∀ k ≤ n, Filter.Tendsto (fun (i : ι) => (g i).coeff k) l (nhds (g₀.coeff k))) : Filter.Tendsto (fun (i : ι) => (f i).resultant (g i) m n) l (nhds (f₀.resultant g₀ m n))

The resultant at fixed formal degrees m and n depends continuously on the coefficients: if, along a filter, the coefficients of index at most m of f i and those of index at most n of g i converge to those of f₀ and g₀, then the resultants converge.

theorem TauCeti.Polynomial.continuous_coeff_monicOfCoeff {R : Type u_1} [CommSemiring R] [TopologicalSpace R] {n : ℕ} (j : ℕ) : Continuous fun (a : Fin n → R) => (monicOfCoeff a).coeff j

Each coefficient of the monic polynomial monicOfCoeff a is a continuous function of the coefficient tuple a: it is either constant or a coordinate of a.

theorem TauCeti.Polynomial.continuous_coeff_prod_X_sub_C {ι : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (s : Finset ι) (k : ℕ) : Continuous fun (f : ι → R) => (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).coeff k

The coefficients of ∏ i ∈ s, (X - C (f i)) depend continuously on the tuple f of roots.

Each coefficient is, up to sign, an elementary symmetric function of the roots, so continuity of the ring operations is all that is used.