Evaluation is multiplicative on the closed polydisc, over K = ℝ or ℂ

For two series of finite ρ-norm and ‖x_k‖ ≤ ρ_k, the product of the two absolutely convergent sums is the sum over all pairs of exponents (tsum_mul_tsum_of_summable_norm), which regrouped by the sum of the two exponents (hasSum_sum_antidiagonal) is the sum of the Cauchy-product coefficients ∑_{μ + μ' = ν} a_μ b_{μ'} times x^ν, the coefficients of f g (MvPowerSeries.coeff_mul). Standard [GR71, Kapitel I]; it is what makes evaluation a ring homomorphism from the convergent series to the functions on a polydisc.

theorem Analytic.evalSeries_mul {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f g : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) (hg : ConvNorm (↑ρ) g ≠ ⊤) {x : Fin m → K} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(↑ρ k)) : evalSeries (f * g) x = evalSeries f x * evalSeries g x

Evaluation is multiplicative on the closed polydisc.

@[simp]

theorem Analytic.evalSeries_zero_eq {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) : evalSeries f 0 = MvPowerSeries.constantCoeff f

Evaluation at 0 is the constant coefficient.

theorem Analytic.evalSeries_one {K : Type u_1} [RCLike K] {m : ℕ} (x : Fin m → K) : evalSeries 1 x = 1

The function of the series 1 is the constant 1.