Swapping circle integrals with infinite sums #
This file proves circleIntegral_tsum, which allows swapping a circle integral
with a tsum under dominated convergence conditions.
theorem
circleIntegral_tsum
{c : ℂ}
{R : ℝ}
{f : ℤ → ℂ → ℂ}
{g : ℂ → ℂ}
(hR : 0 < R)
(hsum : ∀ z ∈ Metric.sphere c R, HasSum (fun (n : ℤ) => f n z) (g z))
(hint : ∀ (n : ℤ), CircleIntegrable (f n) c R)
(hunif : ∃ (M : ℤ → ℝ), Summable M ∧ ∀ (n : ℤ), ∀ z ∈ Metric.sphere c R, ‖f n z‖ ≤ M n)
:
Swap a circle integral with an infinite sum (tsum) under dominated convergence.
If f n are circle-integrable functions that are uniformly bounded by a summable
sequence M n on the sphere, and g z = ∑' n, f n z on the sphere, then
∮ z in C(c,R), g z = ∑' n, ∮ z in C(c,R), f n z.