Holomorphic functions summed over the roots of a polynomial

Let g be holomorphic near the roots of a monic complex polynomial P₀. This file proves that the sum ∑ g(z) over the roots z of a monic polynomial P, counted with multiplicity, depends analytically on the coefficients of P near those of P₀, with no assumption that the roots of P₀ are distinct. By Newton's identities the same then holds for the elementary symmetric functions of the values g(z), that is, for the coefficients of ∏ (X - g(z)).

Read through the elementary symmetric chart TauCeti.Sym.coeffEquiv, which identifies Sym^n ℂ with Fin n → ℂ, this says that a holomorphic change of coordinate φ acts analytically on elementary symmetric coordinates everywhere, including along the diagonal where points collide: TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt. This is the local analytic input needed to prove that the transition maps of the elementary symmetric atlas on the symmetric power of a Riemann surface are holomorphic (Ozsváth--Szabó, arXiv:math/0101206, §2.1). At tuples of distinct points the same local conclusion is TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm, obtained there from the implicit function theorem, which is unavailable once roots collide.

The argument

Around each distinct root w of P₀ choose a small circle C(w, r), the closed discs being pairwise disjoint and inside the region where g is holomorphic. By the argument principle weighted by g (Ahlfors, Complex Analysis, Ch. 4, §5.2),

(2πi)⁻¹ ∮_{C(w, r)} g(t) P'(t) / P(t) dt = ∑_{z root of P, |z - w| < r} g(z),

and for P near P₀ every root of P lies in one of the discs, by continuity of the roots (TauCeti.Sym.coeffHomeomorph). Summing over w expresses ∑ g(z) as a finite sum of contour integrals; summing only over the w lying in a region U whose frontier contains no root of P₀ expresses the sum over the roots in U. Each of these is analytic in the coefficients c of P: restricted to the circle, P and P' are affine functions of c with values in the Banach algebra C(sphere w r, ℂ), P₀ is a unit there since it does not vanish on the circle, inversion is analytic on the units of a Banach algebra (analyticAt_inverse), and integration over the circle is a continuous linear functional on C(sphere w r, ℂ).

Main results

• Polynomial.circleIntegral_mul_derivative_div_eval: the argument principle for a polynomial, weighted by a holomorphic function.
• TauCeti.Polynomial.analyticAt_circleIntegral_mul_derivative_div_monicOfCoeff: such a contour integral depends analytically on the coefficients of a monic polynomial not vanishing on the circle.
• TauCeti.analyticAt_esymm_of_forall_analyticAt_sum_map_pow: analyticity passes from the power sums of a family of multisets to its elementary symmetric functions.
• TauCeti.Sym.analyticAt_sum_map_filter_coeffEquiv_symm: sums of a holomorphic function over the roots lying in a region are analytic in the coefficients, colliding roots included, provided no root lies on the frontier of the region; TauCeti.Sym.analyticAt_sum_map_coeffEquiv_symm is the case of the whole plane.
• TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt: a holomorphic coordinate change acts analytically on elementary symmetric coordinates, colliding points included.

theorem TauCeti.Polynomial.analyticAt_circleIntegral_mul_derivative_div_monicOfCoeff {w : ℂ} {r : ℝ} {n : ℕ} {g : ℂ → ℂ} (hr : 0 ≤ r) (hg : ContinuousOn g (Metric.sphere w r)) {c₀ : Fin n → ℂ} (hc₀ : ∀ t ∈ Metric.sphere w r, Polynomial.eval t (monicOfCoeff c₀) ≠ 0) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => ∮ (t : ℂ) in C(w, r), g t * (Polynomial.eval t (Polynomial.derivative (monicOfCoeff c)) / Polynomial.eval t (monicOfCoeff c))) c₀

Contour integrals against the logarithmic derivative of a monic polynomial depend analytically on its coefficients. If the monic polynomial with lower coefficients c₀ does not vanish on the circle C(w, r), and g is continuous there, then c ↦ ∮_{C(w, r)} g(t) P_c'(t) / P_c(t) dt, where P_c is the monic polynomial with lower coefficients c, is analytic at c₀.

theorem Polynomial.circleIntegral_mul_derivative_div_eval {w : ℂ} {r : ℝ} {g : ℂ → ℂ} (p : Polynomial ℂ) (hr : 0 < r) (hg : DiffContOnCl ℂ g (Metric.ball w r)) (hp : ∀ z ∈ p.roots, z ∉ Metric.sphere w r) : ∮ (t : ℂ) in C(w, r), g t * (eval t (derivative p) / eval t p) = 2 * ↑Real.pi * Complex.I * (Multiset.map g (Multiset.filter (fun (x : ℂ) => x ∈ Metric.ball w r) p.roots)).sum

The argument principle for a polynomial, weighted by a holomorphic function. If g is holomorphic on the disc ball w r and continuous up to its boundary, and no root of p lies on the circle C(w, r), then integrating g against the logarithmic derivative p' / p over the circle gives 2πi times the sum of the values of g at the roots of p inside, counted with multiplicity.

theorem TauCeti.Sym.analyticAt_sum_map_filter_coeffEquiv_symm {n : ℕ} {g : ℂ → ℂ} {U : Set ℂ} [DecidablePred fun (x : ℂ) => x ∈ U] {c₀ : Fin n → ℂ} (hU : ∀ z ∈ (coeffEquiv ℂ n).symm c₀, z ∉ frontier U) (hg : ∀ z ∈ (coeffEquiv ℂ n).symm c₀, z ∈ U → AnalyticAt ℂ g z) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => (Multiset.map g (Multiset.filter (fun (x : ℂ) => x ∈ U) ↑((coeffEquiv ℂ n).symm c))).sum) c₀

Sums of a holomorphic function over the roots in a region depend analytically on the coefficients. Let U be a set of complex numbers whose frontier contains no point of the unordered tuple with elementary symmetric coordinates c₀, and let g be holomorphic at every point of that tuple lying in U. Then c ↦ ∑ g(z), the sum running over the points z of the tuple with coordinates c that lie in U, counted with multiplicity, is analytic at c₀. No distinctness is assumed: the points of the tuple may collide.

theorem TauCeti.Sym.analyticAt_sum_map_coeffEquiv_symm {n : ℕ} {g : ℂ → ℂ} {c₀ : Fin n → ℂ} (hg : ∀ z ∈ (coeffEquiv ℂ n).symm c₀, AnalyticAt ℂ g z) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => (Multiset.map g ↑((coeffEquiv ℂ n).symm c)).sum) c₀

Sums of a holomorphic function over the roots depend analytically on the coefficients. If g is holomorphic at every point of the unordered tuple with elementary symmetric coordinates c₀, then c ↦ ∑ g(z), the sum running over the points z of the tuple with coordinates c, counted with multiplicity, is analytic at c₀. No distinctness is assumed: the points of the tuple may collide.

theorem TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt {n : ℕ} {φ : ℂ → ℂ} {c₀ : Fin n → ℂ} (hφ : ∀ z ∈ (coeffEquiv ℂ n).symm c₀, AnalyticAt ℂ φ z) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => (coeffEquiv ℂ n) (Sym.map φ ((coeffEquiv ℂ n).symm c))) c₀

A holomorphic coordinate change acts analytically on elementary symmetric coordinates, also where points collide. A map φ of ℂ induces a map of coefficient tuples, sending the lower coefficients of a monic polynomial to those of the monic polynomial whose roots are the φ-images of its roots. This induced map is analytic at every coefficient tuple c₀ at each of whose roots φ is analytic, whether or not those roots are distinct.

Read on the symmetric power of a Riemann surface, this is the local analytic input for the holomorphy of the corresponding transition map of elementary symmetric charts.