Theorem: sum_integral_commute
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f n (circleMap c r θ))
    (∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • g (circleMap c r θ))
Tactic:
apply intervalIntegral.hasSum_integral_of_dominated_convergence fun n _ ↦ r * b n
Proof state after:
case hF_meas
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ (n : ℕ),
    MeasureTheory.AEStronglyMeasurable (fun t => (circleMap 0 r t * I) • f n (circleMap c r t))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))

case h_bound
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ (n : ℕ),
    ∀ᵐ (t : ℝ) ∂MeasureTheory.volume, t ∈ Ι 0 (2 * π) → ‖(circleMap 0 r t * I) • f n (circleMap c r t)‖ ≤ r * b n

case bound_summable
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume, t ∈ Ι 0 (2 * π) → Summable fun n => r * b n

case bound_integrable
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ IntervalIntegrable (fun t => ∑' (n : ℕ), r * b n) MeasureTheory.volume 0 (2 * π)

case h_lim
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume,
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n => (circleMap 0 r t * I) • f n (circleMap c r t)) ((circleMap 0 r t * I) • g (circleMap c r t))