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.

Main results

• 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.

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

If every coefficient of two polynomial families is continuous at x₀, then so is every coefficient of their product.

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

If every coefficient of each member of a finite family of polynomial families is continuous at x₀, then so is every coefficient of their product.

theorem Polynomial.continuous_eval_of_continuous_coeff {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [CommSemiring R] [TopologicalSpace 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.