Analyticity on the open polydisc, by rescaling, over K = ℝ or ℂ

HasFPowerSeriesOnBall lives on a sup-norm ball, while a series of finite ρ-norm converges on the polydisc {x | ∀ k, ‖x_k‖ < ρ_k}. The two are reconciled by rescaling the coefficients: rescale ρ f = ∑_ν a_ν ρ^ν x^ν has finite norm at the constant radius 1, its function is evalSeries f (ρ · y), and the polydisc is the image of the unit ball under y ↦ ρ · y. So evalSeries f = evalSeries (rescale ρ f) ∘ (x ↦ x / ρ) is analytic at every point of the open polydisc, as the composition of a function analytic on the unit ball with a continuous linear map. Over ℝ the polydisc is the open box ∏_k (-ρ_k, ρ_k). Standard [GR71, Kapitel I].

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

The series with coefficients a_ν ρ^ν.

Equations

• Analytic.rescale ρ f ν = (MvPowerSeries.coeff ν) f * ↑↑(Analytic.monomialEval ρ ν)

theorem Analytic.coeff_rescale {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f : MvPowerSeries (Fin m) K) (ν : Fin m →₀ ℕ) : (MvPowerSeries.coeff ν) (rescale ρ f) = (MvPowerSeries.coeff ν) f * ↑↑(monomialEval ρ ν)

theorem Analytic.convNorm_rescale {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f : MvPowerSeries (Fin m) K) : ConvNorm (fun (x : Fin m) => 1) (rescale ρ f) = ConvNorm ρ f

The rescaled series has, at the constant radius 1, the norm of f at ρ.

theorem Analytic.coe_monomialEval_eq_prod {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (ν : Fin m →₀ ℕ) : ↑↑(monomialEval ρ ν) = ν.prod fun (k : Fin m) (n : ℕ) => ↑↑(ρ k) ^ n

The real weight ρ^ν in K is the product of the coerced entries.

theorem Analytic.monomialEval_mul_left {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (y : Fin m → K) (ν : Fin m →₀ ℕ) : monomialEval (fun (k : Fin m) => ↑↑(ρ k) * y k) ν = ↑↑(monomialEval ρ ν) * monomialEval y ν

theorem Analytic.evalSeries_rescale {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f : MvPowerSeries (Fin m) K) (y : Fin m → K) : evalSeries (rescale ρ f) y = evalSeries f fun (k : Fin m) => ↑↑(ρ k) * y k

theorem Analytic.analyticOnNhd_evalSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) : AnalyticOnNhd K (evalSeries f) {x : Fin m → K | ∀ (k : Fin m), ‖x k‖ < ↑(↑ρ k)}

The function of a series of finite ρ-norm is analytic on the open polydisc {x | ∀ k, ‖x_k‖ < ρ_k}.

The real case

theorem Analytic.pi_Ioo_eq_setOf_norm_lt {m : ℕ} (ρ : Radius m) : (Set.univ.pi fun (k : Fin m) => Set.Ioo (-↑(↑ρ k)) ↑(↑ρ k)) = {x : Fin m → ℝ | ∀ (k : Fin m), ‖x k‖ < ↑(↑ρ k)}

The open box ∏_k (-ρ_k, ρ_k) is the real norm-polydisc.