Cauchy's integral formula on a polydisc

The vector-valued iterated Cauchy formula assumes continuity and coordinatewise analyticity on the closed polydisc. It does not depend on the several-variable Osgood theorem.

Cauchy's formula on a polydisc

theorem CarlsonFunctions.SeveralComplexVariables.torusIntegrable_cauchyKernelWithRadii {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ} {R : Fin n → ℝ} (hR : ∀ (i : Fin n), 0 < R i) (hw : ∀ (i : Fin n), ‖w i - c i‖ < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) : TorusIntegrable (fun (z : Fin n → ℂ) => (∏ i : Fin n, (z i - w i)⁻¹) • f z) c R

The vector-valued Cauchy kernel of a continuous function is integrable on a torus whenever the evaluation point lies in the interior polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.cauchyKernel_cons {n : ℕ} (x : ℂ) (y : Fin n → ℂ) (w : Fin (n + 1) → ℂ) : ∏ i : Fin (n + 1), (Fin.cons x y i - w i)⁻¹ = (x - w 0)⁻¹ * ∏ i : Fin n, (y i - w i.succ)⁻¹

Splitting off the first coordinate factors the finite-product Cauchy kernel.

theorem CarlsonFunctions.SeveralComplexVariables.polydisc_cauchyWithRadii {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {n : ℕ} {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ} {R : Fin n → ℝ} (hR : ∀ (i : Fin n), 0 < R i) (hw : ∀ (i : Fin n), ‖w i - c i‖ < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin n), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) : (((2 * ↑Real.pi * Complex.I) ^ n)⁻¹ • ∯ (z : Fin n → ℂ) in T(c, R), (∏ i : Fin n, (z i - w i)⁻¹) • f z) = f w

Iterated Cauchy integral formula on a closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.torusIntegrable_cauchyKernel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ} {R : ℝ} (hR : 0 < R) (hw : ∀ (i : Fin n), ‖w i - c i‖ < R) (hfc : ContinuousOn f (closedPolydisc c R)) : TorusIntegrable (fun (z : Fin n → ℂ) => (∏ i : Fin n, (z i - w i)⁻¹) • f z) c fun (x : Fin n) => R

Equal-radius compatibility form of Cauchy-kernel integrability.

theorem CarlsonFunctions.SeveralComplexVariables.polydisc_cauchy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {n : ℕ} {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ} {R : ℝ} (hR : 0 < R) (hw : ∀ (i : Fin n), ‖w i - c i‖ < R) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin n), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) : (((2 * ↑Real.pi * Complex.I) ^ n)⁻¹ • ∯ (z : Fin n → ℂ) in T(c, fun (x : Fin n) => R), (∏ i : Fin n, (z i - w i)⁻¹) • f z) = f w

Equal-radius compatibility form of the polydisc Cauchy formula.