Multivariable Cauchy coefficients and series

Cauchy coefficients, their estimates, and their packaging as a FormalMultilinearSeries. hasFPowerSeriesOnBall_polydiscCauchy_full represents the function on the entire open equal-radius polydisc. The original half-radius theorem remains as a compatibility wrapper. Diagonal coefficients are identified with iterated Fréchet derivatives.

Apply Mathlib's HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn and HasFPowerSeriesOnBall.uniform_geometric_approx to obtain locally uniform partial-sum convergence and geometric remainder bounds on smaller polydiscs. Individual mixed coefficients and radius independence are developed in CauchyCoefficients; the separate-radius multi-index expansion, its uniform convergence and remainder estimates are in PolydiscTaylor.

Multi-index Cauchy series

noncomputable def CarlsonFunctions.SeveralComplexVariables.multiIndexMonomial {d n : ℕ} (m : Fin d → ℕ) (hm : ∑ i : Fin d, m i = n) : (Fin d → ℂ) [×n]→L[ℂ] ℂ

The continuous multilinear monomial associated to a multi-index of total degree n.

Equations

• One or more equations did not get rendered due to their size.

theorem CarlsonFunctions.SeveralComplexVariables.multiIndexMonomial_apply {d n : ℕ} (m : Fin d → ℕ) (hm : ∑ i : Fin d, m i = n) (w : Fin d → ℂ) : ((multiIndexMonomial m hm) fun (x : Fin n) => w) = ∏ i : Fin d, w i ^ m i

On the diagonal, multiIndexMonomial evaluates to the usual multi-index monomial.

theorem CarlsonFunctions.SeveralComplexVariables.norm_multiIndexMonomial_le {d n : ℕ} (m : Fin d → ℕ) (hm : ∑ i : Fin d, m i = n) : ‖multiIndexMonomial m hm‖ ≤ 1

The operator norm of multiIndexMonomial is at most one for the sup norm.

theorem CarlsonFunctions.SeveralComplexVariables.summable_norm_pi_geometric {K : Type u_2} [NormedCommRing K] {d : ℕ} (x : Fin d → K) (hx : ∀ (i : Fin d), ‖x i‖ < 1) : Summable fun (m : Fin d → ℕ) => ‖∏ i : Fin d, x i ^ m i‖

Absolute summability of a finite product of geometric series.

theorem CarlsonFunctions.SeveralComplexVariables.hasSum_pi_geometric {K : Type u_2} [NormedField K] [CompleteSpace K] {d : ℕ} (x : Fin d → K) (hx : ∀ (i : Fin d), ‖x i‖ < 1) : HasSum (fun (m : Fin d → ℕ) => ∏ i : Fin d, x i ^ m i) (∏ i : Fin d, (1 - x i)⁻¹)

The multivariable geometric series sums to the product of its one-variable sums.

noncomputable def CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} (f : (Fin d → ℂ) → E) (c : Fin d → ℂ) (R : ℝ) (m : Fin d → ℕ) : E

The multi-index Cauchy coefficient of a vector-valued function on a polydisc.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CarlsonFunctions.SeveralComplexVariables.polydiscCauchySeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} (f : (Fin d → ℂ) → E) (c : Fin d → ℂ) (R : ℝ) : FormalMultilinearSeries ℂ (Fin d → ℂ) E

The formal multilinear series obtained by grouping the polydisc Cauchy coefficients by total degree.

Equations

• One or more equations did not get rendered due to their size.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscCauchySeries_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d n : ℕ} (f : (Fin d → ℂ) → E) (c h : Fin d → ℂ) (R : ℝ) : ((polydiscCauchySeries f c R n) fun (x : Fin n) => h) = ∑ m : ↥(Finset.Nat.antidiagonalTuple d n), (∏ i : Fin d, h i ^ ↑m i) • polydiscCauchyCoeff f c R ↑m

Evaluation of the homogeneous terms of polydiscCauchySeries on the diagonal.

theorem CarlsonFunctions.SeveralComplexVariables.norm_polydiscCauchyCoeff_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R M : ℝ} (hR : 0 < R) (hM : ∀ z ∈ closedPolydisc c R, ‖f z‖ ≤ M) (m : Fin d → ℕ) : ‖polydiscCauchyCoeff f c R m‖ ≤ M * R⁻¹ ^ ∑ i : Fin d, m i

Cauchy's coefficient estimate for the multi-index coefficients of a bounded function on a closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.hasSum_torusIntegral_of_uniform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} {κ : Type u_2} [Countable κ] {F : κ → (Fin d → ℂ) → E} {g : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} {a : κ → ℝ} (ha : Summable a) (hFint : ∀ (n : κ), TorusIntegrable (F n) c R) (hbound : ∀ (n : κ) (θ : Fin d → ℝ), ‖F n (torusMap c R θ)‖ ≤ a n) (hsum : ∀ (θ : Fin d → ℝ), HasSum (fun (n : κ) => F n (torusMap c R θ)) (g (torusMap c R θ))) : HasSum (fun (n : κ) => torusIntegral (F n) c R) (torusIntegral g c R)

A uniformly absolutely summable series may be integrated termwise on a torus.

theorem CarlsonFunctions.SeveralComplexVariables.hasSum_polydiscCauchySeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {d : ℕ} {f : (Fin d → ℂ) → E} {c h : Fin d → ℂ} {R M : ℝ} (hR : 0 < R) (hh : ∀ (i : Fin d), ‖h i‖ < R) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) (hM : ∀ z ∈ closedPolydisc c R, ‖f z‖ ≤ M) : HasSum (fun (n : ℕ) => (polydiscCauchySeries f c R n) fun (x : Fin n) => h) (f (c + h))

The Cauchy series converges to the function at every point of the open polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.hasFPowerSeriesOnBall_polydiscCauchy_full {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {d : ℕ} {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R M : ℝ} (hR : 0 < R) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) (hM : ∀ z ∈ closedPolydisc c R, ‖f z‖ ≤ M) : HasFPowerSeriesOnBall f (polydiscCauchySeries f c R) c (ENNReal.ofReal R)

The Cauchy series represents the function on the full open supremum-norm ball, not just the half-radius ball needed by the original Osgood proof.

theorem CarlsonFunctions.SeveralComplexVariables.hasFPowerSeriesOnBall_polydiscCauchy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {d : ℕ} {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R M : ℝ} (hR : 0 < R) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) (hM : ∀ z ∈ closedPolydisc c R, ‖f z‖ ≤ M) : HasFPowerSeriesOnBall f (polydiscCauchySeries f c R) c (ENNReal.ofReal (R / 2))

A continuous, separately analytic function on a closed polydisc is represented on the concentric polydisc of half the radius by its multivariable Cauchy series.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscCauchySeries_diag_eq_iteratedFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {d : ℕ} {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R M : ℝ} (hR : 0 < R) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) (hM : ∀ z ∈ closedPolydisc c R, ‖f z‖ ≤ M) (n : ℕ) (v : Fin d → ℂ) : ((polydiscCauchySeries f c R n) fun (x : Fin n) => v) = (↑n.factorial)⁻¹ • (iteratedFDeriv ℂ n f c) fun (x : Fin n) => v

On the diagonal, the Cauchy series is the usual Taylor series of iterated Fréchet derivatives. This uses Mathlib's general coefficient theorem, not a new derivative theory.