The multivariable Cauchy integral formula on polydiscs, proved by coordinate induction.

noncomputable def KamProject.Arnold1963.cauchyKernel {n : ℕ} (w z : ComplexSpace n) : ℂ

The product Cauchy kernel for integration on a polydisc boundary.

Equations

• KamProject.Arnold1963.cauchyKernel w z = ∏ i : Fin n, (z i - w i)⁻¹

theorem KamProject.Arnold1963.continuous_torusMap {n : ℕ} (c : ComplexSpace n) (r : RealSpace n) : Continuous (torusMap c r)

theorem KamProject.Arnold1963.torusMap_mem_pi_closedBall {n : ℕ} (c : ComplexSpace n) {r : RealSpace n} (hr : ∀ (i : Fin n), 0 ≤ r i) (t : RealSpace n) : torusMap c r t ∈ Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (r i)

theorem KamProject.Arnold1963.torusMap_sub_ne_zero {n : ℕ} {c w : ComplexSpace n} {r : RealSpace n} (hw : ∀ (i : Fin n), w i ∈ Metric.ball (c i) (r i)) (t : RealSpace n) (i : Fin n) : torusMap c r t i - w i ≠ 0

theorem KamProject.Arnold1963.continuous_cauchy_boundary {n : ℕ} {f : ComplexSpace n → ℂ} {c w : ComplexSpace n} {r : RealSpace n} (hr : ∀ (i : Fin n), 0 ≤ r i) (hf : ContinuousOn f (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (r i))) (hw : ∀ (i : Fin n), w i ∈ Metric.ball (c i) (r i)) : Continuous fun (t : Fin n → ℝ) => cauchyKernel w (torusMap c r t) * f (torusMap c r t)

theorem KamProject.Arnold1963.polydisc_cauchy {n : ℕ} {f : ComplexSpace n → ℂ} {c w : ComplexSpace n} {r : RealSpace n} (hr : ∀ (i : Fin n), 0 < r i) (hf : AnalyticOnNhd ℂ f (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (r i))) (hw : ∀ (i : Fin n), w i ∈ Metric.ball (c i) (r i)) : (∯ (z : Fin n → ℂ) in T(c, r), cauchyKernel w z * f z) = (2 * ↑Real.pi * Complex.I) ^ n * f w