Theorems · Theorem · complex analysis

TendstoUniformlyOn.tendsto_circleIntegral_of_continuousOn

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ι : Type u_2} {f : ι → ℂ → E} {g : ℂ → E}
  {c : ℂ} {R : ℝ} {l : Filter ι} [l.IsCountablyGenerated],
  0 ≤ R →
    (∀ᶠ (i : ι) in l, ContinuousOn (f i) (Metric.sphere c R)) →
      TendstoUniformlyOn f g l (Metric.sphere c R) →
        Filter.Tendsto (fun n => ∮ (z : ℂ) in C(c, R), f n z) l (nhds (∮ (z : ℂ) in C(c, R), g z))

If a sequence of continuous functions converges uniformly on the circle, then their circle integrals converge to the circle integral of the limit function.

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

0 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFilter.IsCountablyGenerated