Evaluation of a convergent series over K = ℝ or ℂ, and its power series at 0

For a series f of finite ρ-norm and a point x ∈ K^m of the closed polydisc ‖x_k‖ ≤ ρ_k, the terms a_ν x^ν are dominated by ‖a_ν‖ ρ^ν, so the sum evalSeries f x = ∑_ν a_ν x^ν converges absolutely (summable_norm_evalTerm, hasSum_evalSeries). Regrouped by degree, the sum is the value at x of the formal multilinear series toFMS f, whose degree-n term is ∑_{|ν| = n} a_ν · monoMapExp n ν with monoMapExp n ν (v₁, …, vₙ) = ∏_i (v_i)_{k_i} for an enumeration k of ν; its norm is at most ∑_{|ν| = n} ‖a_ν‖, so the radius of toFMS f is at least min_k ρ_k and evalSeries f has this power series on the sup-norm ball (hasFPowerSeriesOnBall_evalSeries), hence is analytic there, with iterated derivatives at 0 given by the coefficients (factorial_smul_sum_eq_iteratedFDeriv); a monomial sums to itself (evalSeries_monomial, evalSeries_X_pow). Standard material [GR71, Kapitel I], phrased through Mathlib's HasFPowerSeriesOnBall; analyticity on the whole open polydisc is in Rescale.lean, and the converse (an analytic function is the sum of a convergent series) in Bridge.lean.

theorem Analytic.norm_monomialEval_le {K : Type u_1} [RCLike K] {m : ℕ} {x : Fin m → K} {ρ : Fin m → NNReal} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(ρ k)) (ν : Fin m →₀ ℕ) : ‖monomialEval x ν‖ ≤ ↑(monomialEval ρ ν)

On the closed polydisc ‖x_k‖ ≤ ρ_k the monomials are dominated by ρ^ν.

Evaluation and absolute convergence

noncomputable def Analytic.evalSeries {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) (x : Fin m → K) : K

The function x ↦ ∑_ν a_ν x^ν defined by a formal power series (the sum is the tsum; it is meaningful on the polydisc of a radius vector with finite norm).

Equations

• Analytic.evalSeries f x = ∑' (ν : Fin m →₀ ℕ), (MvPowerSeries.coeff ν) f * Analytic.monomialEval x ν

theorem Analytic.summable_weighted {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) : Summable fun (ν : Fin m →₀ ℕ) => ‖(MvPowerSeries.coeff ν) f‖ * ↑(monomialEval (↑ρ) ν)

The weighted coefficients ‖a_ν‖ ρ^ν of a series of finite ρ-norm are summable.

theorem Analytic.summable_norm_evalTerm {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {x : Fin m → K} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(↑ρ k)) : Summable fun (ν : Fin m →₀ ℕ) => ‖(MvPowerSeries.coeff ν) f * monomialEval x ν‖

On the closed polydisc ‖x_k‖ ≤ ρ_k the series converges absolutely (its terms are dominated by ‖a_ν‖ ρ^ν, uniformly in x).

theorem Analytic.hasSum_evalSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {x : Fin m → K} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(↑ρ k)) : HasSum (fun (ν : Fin m →₀ ℕ) => (MvPowerSeries.coeff ν) f * monomialEval x ν) (evalSeries f x)

The multilinear terms

noncomputable def Analytic.monoMap (K : Type u_1) [RCLike K] {m : ℕ} (n : ℕ) (k : Fin n → Fin m) : (Fin m → K) [×n]→L[K] K

The continuous multilinear map (v₁, …, vₙ) ↦ ∏ i, v_i (k i) attached to a tuple k of coordinate indices.

Equations

• Analytic.monoMap K n k = (ContinuousMultilinearMap.mkPiAlgebraFin K n K).compContinuousLinearMap fun (i : Fin n) => ContinuousLinearMap.proj (k i)

theorem Analytic.monoMap_apply {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) (k : Fin n → Fin m) (v : Fin n → Fin m → K) : (monoMap K n k) v = ∏ i : Fin n, v i (k i)

theorem Analytic.norm_monoMap_le {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) (k : Fin n → Fin m) : ‖monoMap K n k‖ ≤ 1

noncomputable def Analytic.monoMapExp (K : Type u_1) [RCLike K] {m : ℕ} (n : ℕ) (ν : Fin m →₀ ℕ) : (Fin m → K) [×n]→L[K] K

The multilinear map of a single exponent ν in degree n: monoMap of the enumeration of ν when |ν| = n, and 0 otherwise.

Equations

• Analytic.monoMapExp K n ν = if h : (Analytic.expList ν).length = n then Analytic.monoMap K n fun (i : Fin n) => (Analytic.expList ν).get (Fin.cast ⋯ i) else 0

theorem Analytic.monoMapExp_apply_diag {K : Type u_1} [RCLike K] {m n : ℕ} {ν : Fin m →₀ ℕ} (h : Finsupp.degree ν = n) (x : Fin m → K) : ((monoMapExp K n ν) fun (x_1 : Fin n) => x) = monomialEval x ν

theorem Analytic.norm_monoMapExp_le {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) (ν : Fin m →₀ ℕ) : ‖monoMapExp K n ν‖ ≤ 1

The formal multilinear series and its convergence

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

The formal multilinear series of a power series, ∑_{|ν| = n} a_ν · monoMapExp n ν in degree n.

Equations

• Analytic.toFMS f n = ∑ ν ∈ Analytic.degreeSet m n, (MvPowerSeries.coeff ν) f • Analytic.monoMapExp K n ν

theorem Analytic.toFMS_apply_diag {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) (n : ℕ) (x : Fin m → K) : ((toFMS f n) fun (x_1 : Fin n) => x) = ∑ ν ∈ degreeSet m n, (MvPowerSeries.coeff ν) f * monomialEval x ν

theorem Analytic.norm_toFMS_le {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) (n : ℕ) : ‖toFMS f n‖ ≤ ∑ ν ∈ degreeSet m n, ‖(MvPowerSeries.coeff ν) f‖

theorem Analytic.le_radius_toFMS {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {r : NNReal} (hr : ∀ (k : Fin m), r ≤ ↑ρ k) : ↑r ≤ (toFMS f).radius

The radius of toFMS f is at least any r ≤ min_k ρ_k when ‖f‖_ρ < ∞.

theorem Analytic.hasFPowerSeriesOnBall_evalSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {r : NNReal} (hr0 : 0 < r) (hr : ∀ (k : Fin m), r ≤ ↑ρ k) : HasFPowerSeriesOnBall (evalSeries f) (toFMS f) 0 ↑r

A series of finite ρ-norm has the power series toFMS f at 0 on the sup-norm ball of any radius r ≤ min_k ρ_k (Mathlib's HasFPowerSeriesOnBall).

theorem Analytic.analyticOnNhd_evalSeries_ball {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {r : NNReal} (hr0 : 0 < r) (hr : ∀ (k : Fin m), r ≤ ↑ρ k) : AnalyticOnNhd K (evalSeries f) (Metric.ball 0 ↑r)

The function of a series of finite ρ-norm is analytic on the open sup-norm ball of radius min_k ρ_k (any r ≤ ρ_k).

theorem Analytic.factorial_smul_sum_eq_iteratedFDeriv {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) (n : ℕ) (x : Fin m → K) : n.factorial • ∑ ν ∈ degreeSet m n, (MvPowerSeries.coeff ν) f * monomialEval x ν = (iteratedFDeriv K n (evalSeries f) 0) fun (x_1 : Fin n) => x

The iterated derivatives at 0 are the coefficients up to factorials: n! · ∑_{|ν| = n} a_ν x^ν = D^n (evalSeries f) (0) (x, …, x).

Monomials

theorem Analytic.evalSeries_monomial {K : Type u_1} [RCLike K] {m : ℕ} (ν : Fin m →₀ ℕ) (a : K) (x : Fin m → K) : evalSeries ((MvPowerSeries.monomial ν) a) x = a * monomialEval x ν

The sum of a monomial a x^ν is a x^ν.

theorem Analytic.evalSeries_X_pow {K : Type u_1} [RCLike K] {m : ℕ} (k : Fin m) (n : ℕ) (x : Fin m → K) : evalSeries (MvPowerSeries.X k ^ n) x = x k ^ n

The sum of x_k^n is x_k^n.

theorem Analytic.convNorm_X_pow_ne_top {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (k : Fin m) (n : ℕ) : ConvNorm ρ (MvPowerSeries.X k ^ n) ≠ ⊤

x_k^n has finite majorant norm for every radius vector.

The real case

theorem Analytic.abs_monomialEval_le {m : ℕ} {x : Fin m → ℝ} {ρ : Fin m → NNReal} (hx : ∀ (k : Fin m), |x k| ≤ ↑(ρ k)) (ν : Fin m →₀ ℕ) : |monomialEval x ν| ≤ ↑(monomialEval ρ ν)

On the closed polydisc |x_k| ≤ ρ_k the monomials are dominated by ρ^ν.