Analytic elementary symmetric functions of multisets

Newton's identities express each elementary symmetric function of a multiset in terms of lower elementary symmetric functions and power sums. Consequently, a family of multisets whose power sums through degree k are analytic has analytic k-th elementary symmetric function.

Main declarations

• TauCeti.analyticAt_esymm_of_forall_analyticAt_sum_map_pow: analyticity of the power sums through degree k implies analyticity of the k-th elementary symmetric function.

theorem TauCeti.analyticAt_esymm_of_forall_analyticAt_sum_map_pow {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {m : E → Multiset 𝕜} {x₀ : E} (k : ℕ) (h : ∀ (j : ℕ), 0 < j → j ≤ k → AnalyticAt 𝕜 (fun (x : E) => (Multiset.map (fun (x : 𝕜) => x ^ j) (m x)).sum) x₀) : AnalyticAt 𝕜 (fun (x : E) => (m x).esymm k) x₀

If the power sums through degree k of a family of multisets depend analytically on the parameter, then so does its k-th elementary symmetric function, by Newton's identities.