From analytic functions to convergent series, and uniqueness of coefficients

Mathlib's AnalyticAt is stated over any nontrivially normed field; over K = ℝ or ℂ an analytic function on Fin m → K near a is the function of a convergent power series in x - a, and two convergent series with the same function near 0 are equal. Together with Eval.lean this identifies the ring of convergent series with the ring of germs of analytic functions, an identification the sources take for granted [GR71, Kapitel I]; Mathlib has only the one-variable uniqueness (HasFPowerSeriesAt.eq_formalMultilinearSeries), so the arguments are given here.

The coefficients. If f has the power series p at a on a ball of radius r, the n-th term p n is a continuous multilinear map; expanding each argument y = ∑_j y_j e_j in the coordinate basis (ContinuousMultilinearMap.map_sum_finset, map_smul_univ) gives p n (y, …, y) = ∑_{k : Fin n → Fin m} (∏_i y_{k i}) · p n (e_{k 1}, …, e_{k n}), and grouping the tuples k by their count vector ν(k) = ∑_i single (k i) 1 gives ∑_{|ν| = n} c_ν y^ν with c_ν = ∑_{ν(k) = ν} p n (e_k). No symmetry of p n is used.

The norm. ‖c_ν‖ ≤ #{k : ν(k) = ν} · ‖p n‖, and the fibre counts over |ν| = n add up to m^n, so at the constant radius r' = r / (2 (m + 1)) the degree-n slice of the majorant norm is at most ‖p n‖ (m r')^n, summable because m r' < r ≤ p.radius.

Uniqueness. Two convergent series whose functions agree near 0 have the same iterated derivatives at 0; by factorial_smul_sum_eq_iteratedFDeriv the homogeneous parts agree as functions, hence as polynomials (MvPolynomial.funext, K is infinite), hence coefficientwise.

Expanding a multilinear term in the coordinate basis

theorem Analytic.eq_sum_smul_single {K : Type u_1} [RCLike K] {m : ℕ} (y : Fin m → K) : y = ∑ j : Fin m, y j • Pi.single j 1

y = ∑_j y_j • e_j in Fin m → K.

theorem Analytic.fms_apply_diag_eq_sum {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) (n : ℕ) (y : Fin m → K) : ((p n) fun (x : Fin n) => y) = ∑ k : Fin n → Fin m, (∏ i : Fin n, y (k i)) * (p n) fun (i : Fin n) => Pi.single (k i) 1

A multilinear term on the diagonal, expanded in the coordinate basis.

noncomputable def Analytic.coeffOfFMS {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) : MvPowerSeries (Fin m) K

The coefficients read off a power series, c_ν = ∑_{ν(k) = ν} p |ν| (e_k).

Equations

• Analytic.coeffOfFMS p ν = ∑ k : Fin (Finsupp.degree ν) → Fin m with Analytic.countVec k = ν, (p (Finsupp.degree ν)) fun (i : Fin (Finsupp.degree ν)) => Pi.single (k i) 1

theorem Analytic.coeff_coeffOfFMS {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) {n : ℕ} {ν : Fin m →₀ ℕ} (h : Finsupp.degree ν = n) : (MvPowerSeries.coeff ν) (coeffOfFMS p) = ∑ k : Fin n → Fin m with countVec k = ν, (p n) fun (i : Fin n) => Pi.single (k i) 1

theorem Analytic.fms_apply_diag_eq_sum_coeff {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) (n : ℕ) (y : Fin m → K) : ((p n) fun (x : Fin n) => y) = ∑ ν ∈ degreeSet m n, (MvPowerSeries.coeff ν) (coeffOfFMS p) * monomialEval y ν

The multilinear term on the diagonal is the degree-n part of the series with coefficients coeffOfFMS p.

theorem Analytic.norm_coeff_coeffOfFMS_le {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) {n : ℕ} {ν : Fin m →₀ ℕ} (h : Finsupp.degree ν = n) : ‖(MvPowerSeries.coeff ν) (coeffOfFMS p)‖ ≤ ↑{k : Fin n → Fin m | countVec k = ν}.card * ‖p n‖

‖c_ν‖ ≤ #{k : ν(k) = ν} · ‖p n‖.

The bridge

theorem Analytic.sum_norm_coeffOfFMS_le {K : Type u_1} [RCLike K] {m : ℕ} (p : FormalMultilinearSeries K (Fin m → K) K) (r' : NNReal) (n : ℕ) : ∑ ν ∈ degreeSet m n, ‖(MvPowerSeries.coeff ν) (coeffOfFMS p)‖ * ↑(monomialEval (fun (x : Fin m) => r') ν) ≤ ‖p n‖ * (↑m * ↑r') ^ n

The degree-n slice of the majorant norm of coeffOfFMS p at a constant radius r' is at most ‖p n‖ (m r')^n.

theorem AnalyticAt.exists_conv_coeff {K : Type u_1} [RCLike K] {m : ℕ} {f : (Fin m → K) → K} {a : Fin m → K} (hf : AnalyticAt K f a) : ∃ (ρ : Analytic.Radius m) (c : MvPowerSeries (Fin m) K), Analytic.ConvNorm (↑ρ) c ≠ ⊤ ∧ ∀ (x : Fin m → K), (∀ (k : Fin m), ‖x k‖ < ↑(↑ρ k)) → f (a + x) = Analytic.evalSeries c x

A K-analytic function at a agrees near a with the function of a convergent series in x - a.

Uniqueness of coefficients

noncomputable def Analytic.homogeneousPoly {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) (n : ℕ) : MvPolynomial (Fin m) K

The homogeneous part of degree n as a polynomial.

Equations

• Analytic.homogeneousPoly f n = ∑ ν ∈ Analytic.degreeSet m n, (MvPolynomial.monomial ν) ((MvPowerSeries.coeff ν) f)

theorem Analytic.eval_homogeneousPoly {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) (n : ℕ) (x : Fin m → K) : (MvPolynomial.eval x) (homogeneousPoly f n) = ∑ ν ∈ degreeSet m n, (MvPowerSeries.coeff ν) f * monomialEval x ν

theorem Analytic.coeff_homogeneousPoly {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) {n : ℕ} {ν : Fin m →₀ ℕ} (hν : Finsupp.degree ν = n) : (homogeneousPoly f n).coeff ν = (MvPowerSeries.coeff ν) f

theorem Analytic.eq_of_evalSeries_eventuallyEq {K : Type u_1} [RCLike K] {m : ℕ} {f g : MvPowerSeries (Fin m) K} (hf : f ∈ Conv K m) (hg : g ∈ Conv K m) (h : evalSeries f =ᶠ[nhds 0] evalSeries g) : f = g

Uniqueness of coefficients: two convergent series whose functions agree on a neighbourhood of 0 are equal.

Series centred at a point

theorem Analytic.eventually_norm_sub_lt {K : Type u_1} [RCLike K] {m : ℕ} (a : Fin m → K) (ρ : Radius m) : ∀ᶠ (x : Fin m → K) in nhds a, ∀ (k : Fin m), ‖(x - a) k‖ < ↑(↑ρ k)

The norm-polydisc of radius ρ around a is a neighbourhood of a.

theorem AnalyticAt.exists_eventuallyEq_evalSeries {K : Type u_1} [RCLike K] {m : ℕ} {f : (Fin m → K) → K} {a : Fin m → K} (hf : AnalyticAt K f a) : ∃ (ρ : Analytic.Radius m) (c : MvPowerSeries (Fin m) K), Analytic.ConvNorm (↑ρ) c ≠ ⊤ ∧ f =ᶠ[nhds a] fun (x : Fin m → K) => Analytic.evalSeries c (x - a)

The expansion centred at a: an analytic f agrees near a with the sum of a series of finite majorant norm in x - a.