The Cauchy integral formula on polydiscs and analyticity in several variables

This file proves the iterated Cauchy integral formula on a polydisc, and deduces that a function of finitely many complex variables which is complex differentiable on an open set is analytic there. Mathlib proves both facts for functions of one complex variable (DifferentiableOn.circleIntegral_sub_inv_smul, DifferentiableOn.analyticOnNhd); the several-variable statements are the basic tools for proving joint analyticity of functions defined by parameter-dependent contour integrals. The file ends with the first such statement: a contour integral whose integrand is jointly analytic in a parameter and the integration variable is analytic in the parameter.

A polydisc in ℂⁿ is the product Set.univ.pi fun i => ball (c i) (R i) of open discs, and its distinguished boundary is the torus T(c, R) of Mathlib's torusIntegral.

Main results

• DifferentiableOn.torusIntegral_prod_sub_inv_smul: the Cauchy integral formula on a polydisc. If f : ℂⁿ → E is complex differentiable on the closed polydisc with center c and polyradius R, then for w in the open polydisc, ∯ z in T(c, R), (∏ i, (z i - w i))⁻¹ • f z = (2πi)ⁿ • f w.
• DifferentiableOn.analyticAt_of_finiteDimensional, DifferentiableOn.analyticOnNhd_of_finiteDimensional: a function on a finite-dimensional complex normed space which is complex differentiable on a neighbourhood of a point is analytic there.
• TauCeti.analyticOnNhd_iff_differentiableOn_of_finiteDimensional: on an open subset of a finite-dimensional complex normed space, analyticity and complex differentiability agree.
• TauCeti.hasFDerivAt_circleIntegral: a contour integral p ↦ ∮ ζ in C(c, R), f (p, ζ) whose integrand is jointly analytic along {p} × sphere c |R| may be differentiated under the integral sign at p.
• TauCeti.analyticAt_circleIntegral, TauCeti.analyticOnNhd_circleIntegral: analytic dependence on parameters. For a parameter in a finite-dimensional complex normed space, such a contour integral is analytic in the parameter.

The argument

The Cauchy formula follows by induction on n from the one-variable formula, splitting off the first coordinate of the torus integral with torusIntegral_succ.

For analyticity at z, choose a closed polydisc closedBall z R inside the domain and let X be the torus ∏ sphere (z i) R. On the Banach algebra C(X, ℂ), the Cauchy kernel w ↦ (ζ ↦ ∏ i, (ζ i - w i)) is a polynomial in w, and it is a unit at w = z, so its inverse is analytic in w near z (analyticAt_inverse). Integrating against f over the torus is a continuous linear functional on C(X, ℂ), so by the Cauchy formula f is a continuous linear image of an analytic function near z. This is the several-variable form of the argument in TauCeti.Analysis.Polynomial.RootSum.

For a contour integral depending on a parameter, the partial derivative of the integrand in the parameter is continuous, hence bounded uniformly near the compact circle, so Mathlib's theorem on differentiation under the integral sign applies. Analyticity in a parameter from a finite-dimensional space then follows from complex differentiability on a neighbourhood.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, §2.2.

theorem TauCeti.torusMap_mem_pi_sphere {n : ℕ} {c : Fin n → ℂ} {R : Fin n → ℝ} (hR : ∀ (i : Fin n), 0 ≤ R i) (θ : Fin n → ℝ) : torusMap c R θ ∈ Set.univ.pi fun (i : Fin n) => Metric.sphere (c i) (R i)

For nonnegative radii, a point of the torus T(c, R) lies on the product of the circles sphere (c i) (R i).

theorem TauCeti.continuous_torusMap {n : ℕ} (c : Fin n → ℂ) (R : Fin n → ℝ) : Continuous (torusMap c R)

The parametrization torusMap c R of the torus T(c, R) is continuous.

theorem DifferentiableOn.torusIntegral_prod_sub_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} [CompleteSpace E] {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ} {R : Fin n → ℝ} (hd : DifferentiableOn ℂ f (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (R i))) (hw : w ∈ Set.univ.pi fun (i : Fin n) => Metric.ball (c i) (R i)) : (∯ (z : Fin n → ℂ) in T(c, R), (∏ i : Fin n, (z i - w i))⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) ^ n • f w

The Cauchy integral formula on a polydisc. If f is complex differentiable on the closed polydisc with center c and polyradius R, then for every w in the open polydisc, the integral of (∏ i, (z i - w i))⁻¹ • f z over the distinguished boundary T(c, R) is (2πi)ⁿ • f w.

theorem DifferentiableOn.analyticAt_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {f : V → E} {s : Set V} {z : V} (hd : DifferentiableOn ℂ f s) (hs : s ∈ nhds z) : AnalyticAt ℂ f z

A function on a finite-dimensional complex normed space which is complex differentiable on a neighbourhood of a point is analytic at that point. This is the several-variable form of DifferentiableOn.analyticAt.

theorem DifferentiableOn.analyticOnNhd_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {f : V → E} {s : Set V} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s

A function on a finite-dimensional complex normed space which is complex differentiable on an open set is analytic on it. This is the several-variable form of DifferentiableOn.analyticOnNhd.

theorem TauCeti.analyticOnNhd_iff_differentiableOn_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {f : V → E} {s : Set V} (hs : IsOpen s) : AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

On an open subset of a finite-dimensional complex normed space, a function is analytic if and only if it is complex differentiable. This is the several-variable form of Complex.analyticOnNhd_iff_differentiableOn.

theorem TauCeti.hasFDerivAt_circleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V × ℂ → E} {c : ℂ} {R : ℝ} {p : V} (hf : ∀ ζ ∈ Metric.sphere c |R|, AnalyticAt ℂ f (p, ζ)) : HasFDerivAt (fun (q : V) => ∮ (ζ : ℂ) in C(c, R), f (q, ζ)) (∮ (ζ : ℂ) in C(c, R), fderiv ℂ f (p, ζ) ∘SL ContinuousLinearMap.inl ℂ V ℂ) p

Differentiation of a contour integral under the integral sign. If f is jointly analytic at every point of {p} × sphere c |R|, then q ↦ ∮ ζ in C(c, R), f (q, ζ) has derivative at p the contour integral of the partial derivative of f in the parameter.

theorem TauCeti.analyticAt_circleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V × ℂ → E} {c : ℂ} {R : ℝ} [FiniteDimensional ℂ V] {p₀ : V} (hf : ∀ ζ ∈ Metric.sphere c |R|, AnalyticAt ℂ f (p₀, ζ)) : AnalyticAt ℂ (fun (p : V) => ∮ (ζ : ℂ) in C(c, R), f (p, ζ)) p₀

Analytic dependence of a contour integral on a parameter. If f is jointly analytic at every point of {p₀} × sphere c |R|, then p ↦ ∮ ζ in C(c, R), f (p, ζ) is analytic at p₀.

theorem TauCeti.analyticOnNhd_circleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V × ℂ → E} {c : ℂ} {R : ℝ} [FiniteDimensional ℂ V] {s : Set V} (hf : AnalyticOnNhd ℂ f (s ×ˢ Metric.sphere c |R|)) : AnalyticOnNhd ℂ (fun (p : V) => ∮ (ζ : ℂ) in C(c, R), f (p, ζ)) s

Analytic dependence of a contour integral on a parameter. If f is jointly analytic on a neighbourhood of s × sphere c |R|, then p ↦ ∮ ζ in C(c, R), f (p, ζ) is analytic on a neighbourhood of s.