Taylor expansions on polydiscs with separate radii

The multi-index Cauchy series converges throughout its open polydisc, not merely on the largest inscribed equal-radius ball. Convergence is uniform on smaller closed polydiscs and locally uniform on the full open polydisc, also after mixed differentiation. Explicit geometric-tail estimates control the remainder after any finite set of multi-indices. Scalar Taylor coefficients also define an element of Mathlib's MvPowerSeries.

noncomputable def CarlsonFunctions.SeveralComplexVariables.holomorphicTaylorSeries {d : ℕ} (f : (Fin d → ℂ) → ℂ) (c : Fin d → ℂ) : MvPowerSeries (Fin d) ℂ

The scalar Taylor series as an existing Mathlib multivariate formal power series.

Equations

• CarlsonFunctions.SeveralComplexVariables.holomorphicTaylorSeries f c m = (∏ i : Fin d, ↑(m i).factorial)⁻¹ * CarlsonFunctions.SeveralComplexVariables.multiIndexDeriv (⇑m) f c

theorem CarlsonFunctions.SeveralComplexVariables.coeff_holomorphicTaylorSeries {d : ℕ} {f : (Fin d → ℂ) → ℂ} {c : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (m : Fin d →₀ ℕ) : (MvPowerSeries.coeff m) (holomorphicTaylorSeries f c) = polydiscCauchyCoeffWithRadii f c R ⇑m

Formal Taylor coefficients coincide with the integral Cauchy coefficients.

theorem CarlsonFunctions.SeveralComplexVariables.hasSum_multiIndex_cauchyKernel {d : ℕ} {z c h : Fin d → ℂ} (hz : ∀ (i : Fin d), z i ≠ c i) (hh : ∀ (i : Fin d), ‖h i‖ < ‖z i - c i‖) : HasSum (fun (m : Fin d → ℕ) => (∏ i : Fin d, h i ^ m i) * cauchyKernel m c z) (∏ i : Fin d, (z i - (c + h) i)⁻¹)

The ungrouped multi-index geometric expansion of the Cauchy kernel.

theorem CarlsonFunctions.SeveralComplexVariables.torusIntegrable_cauchyKernel_multi {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin d → ℂ) → E} {c w : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hw : w ∈ polydiscWithRadii c R) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (m : Fin d → ℕ) : TorusIntegrable (fun (z : Fin d → ℂ) => cauchyKernel m w z • f z) c R

Every higher Cauchy kernel times a continuous function is integrable on its contour.

theorem CarlsonFunctions.SeveralComplexVariables.hasSum_polydiscTaylor {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c h : Fin d → ℂ} {R : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hh : ∀ (i : Fin d), ‖h i‖ < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) : HasSum (fun (m : Fin d → ℕ) => (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m) (f (c + h))

The full multi-index Taylor expansion on a polydisc with separate radii. The sum is indexed by all multi-indices, and therefore does not depend on a summation order.

theorem CarlsonFunctions.SeveralComplexVariables.norm_polydiscTaylor_term_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin d → ℂ) → E} {c h : Fin d → ℂ} {R s : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hM0 : 0 ≤ M) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (hh : ∀ (i : Fin d), ‖h i‖ ≤ s i) (m : Fin d → ℕ) : ‖(∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m‖ ≤ M * ∏ i : Fin d, (s i / R i) ^ m i

A summable geometric majorant for individual Taylor terms on a smaller closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.hasSumUniformlyOn_polydiscTaylor {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R s : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hs : ∀ (i : Fin d), 0 ≤ s i) (hsR : ∀ (i : Fin d), s i < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) : HasSumUniformlyOn (fun (m : Fin d → ℕ) (h : Fin d → ℂ) => (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m) (fun (h : Fin d → ℂ) => f (c + h)) (closedPolydiscWithRadii 0 s)

Uniform convergence of the Taylor series on every strictly smaller closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.hasSumLocallyUniformlyOn_polydiscTaylor {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) : HasSumLocallyUniformlyOn (fun (m : Fin d → ℕ) (h : Fin d → ℂ) => (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m) (fun (h : Fin d → ℂ) => f (c + h)) (polydiscWithRadii 0 R)

The multi-index Taylor expansion converges locally uniformly throughout its polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.norm_polydiscTaylor_remainder_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c h : Fin d → ℂ} {R s : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hs : ∀ (i : Fin d), 0 ≤ s i) (hsR : ∀ (i : Fin d), s i < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (hh : ∀ (i : Fin d), ‖h i‖ ≤ s i) (t : Finset (Fin d → ℕ)) : ‖f (c + h) - ∑ m ∈ t, (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m‖ ≤ ∑' (m : { m : Fin d → ℕ // m ∉ t }), M * ∏ i : Fin d, (s i / R i) ^ ↑m i

A uniform remainder bound for any finite Taylor polynomial. The right-hand side is the tail of an explicitly summable product of geometric series.

theorem CarlsonFunctions.SeveralComplexVariables.norm_polydiscTaylor_remainder_le_prod {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c h : Fin d → ℂ} {R s : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hs : ∀ (i : Fin d), 0 ≤ s i) (hsR : ∀ (i : Fin d), s i < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (hh : ∀ (i : Fin d), ‖h i‖ ≤ s i) (t : Finset (Fin d → ℕ)) : ‖f (c + h) - ∑ m ∈ t, (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m‖ ≤ M * (∏ i : Fin d, (1 - s i / R i)⁻¹ - ∑ m ∈ t, ∏ i : Fin d, (s i / R i) ^ m i)

The geometric-tail bound written without an infinite sum: a finite polynomial is subtracted from the product of the geometric sums.

theorem CarlsonFunctions.SeveralComplexVariables.hasSumLocallyUniformlyOn_iteratedPartialDeriv_polydiscTaylor {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (is : List (Fin d)) : HasSumLocallyUniformlyOn (fun (m : Fin d → ℕ) => iteratedPartialDerivCarlson is fun (h : Fin d → ℂ) => (∏ i : Fin d, h i ^ m i) • polydiscCauchyCoeffWithRadii f c R m) (iteratedPartialDerivCarlson is fun (h : Fin d → ℂ) => f (c + h)) (polydiscWithRadii 0 R)

Any mixed derivative of the separate-radius Taylor expansion is obtained by termwise differentiation, with locally uniform convergence on the full open polydisc.