feat(Integral/CircleIntegral): add a convergence theorem (leanprover-community#39204)

From the Riemann mapping theorem project.

Author: urkud

Mathlib/MeasureTheory/Integral/CircleIntegral.lean

@@ -367,6 +367,28 @@ theorem circleIntegral_def_Icc (f : ℂ → E) (c : ℂ) (R : ℝ) :
   rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
     Measure.restrict_congr_set Ioc_ae_eq_Icc]
 
+/-- If a sequence of continuous functions converges uniformly on the circle,
+then their circle integrals converge to the circle integral of the limit function. -/
+theorem _root_.TendstoUniformlyOn.tendsto_circleIntegral_of_continuousOn
+    {ι : Type*} {f : ι → ℂ → E} {g : ℂ → E} {c : ℂ} {R : ℝ}
+    {l : Filter ι} [l.IsCountablyGenerated] (hR : 0 ≤ R)
+    (hf : ∀ᶠ i in l, ContinuousOn (f i) (sphere c R)) (h : TendstoUniformlyOn f g l (sphere c R)) :
+    Tendsto (fun n ↦ ∮ z in C(c, R), f n z) l (𝓝 (∮ z in C(c, R), g z)) := by
+  apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
+  · refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
+    · rw [funext (deriv_circleMap _ _)]
+      fun_prop
+    · fun_prop
+    · simp [hR, MapsTo]
+  · rw [Metric.tendstoUniformlyOn_iff] at h ⊢
+    simp only [dist_smul₀, deriv_circleMap, norm_mul, norm_I, norm_circleMap_zero,
+      abs_of_nonneg hR, mul_one]
+    intro ε hε
+    rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩
+    refine (h δ hδ₀).mono fun i hi x hx ↦ ?_
+    grw [hi (circleMap c R x) (by simp [hR])]
+    exact hRδ
+
 namespace circleIntegral
 
 @[simp]

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+import Mathlib.Topology.Algebra.IsUniformGroup.Order
 
 /-!
 # The dominated convergence theorem
@@ -221,6 +222,26 @@ nonrec theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter
   exact tendsto_const_nhds.smul <|
     tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim
 
+theorem _root_.TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
+    {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E}
+    [IsLocallyFiniteMeasure μ] (hF : ∀ᶠ i in l, ContinuousOn (F i) [[a, b]])
+    (h_lim : TendstoUniformlyOn F f l [[a, b]]) :
+    Tendsto (fun n => ∫ x in a..b, F n x ∂μ) l (𝓝 <| ∫ x in a..b, f x ∂μ) := by
+  rcases l.eq_or_neBot with rfl | hl
+  · simp
+  rcases isCompact_uIcc.bddAbove_image (h_lim.continuousOn hF.frequently).norm with ⟨C, hC⟩
+  apply tendsto_integral_filter_of_dominated_convergence (bound := fun _ ↦ C + 1)
+  case hF_meas =>
+    exact hF.mono fun i hi ↦ hi.mono uIoc_subset_uIcc |>.aestronglyMeasurable measurableSet_uIoc
+  case h_bound =>
+    have := uniformContinuous_norm.comp_tendstoUniformlyOn h_lim
+      |>.eventually_forall_le (show C < C + 1 by simp) (by simpa [upperBounds] using hC)
+    exact this.mono fun i hi ↦ .of_forall fun x hx ↦ hi x <| uIoc_subset_uIcc hx
+  case bound_integrable =>
+    exact intervalIntegrable_const
+  case h_lim =>
+    exact .of_forall fun x hx ↦ h_lim.tendsto_at <| uIoc_subset_uIcc hx
+
 /-- Lebesgue dominated convergence theorem for parametric interval integrals. -/
 nonrec theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → ℝ → E}
     (bound : ι → ℝ → ℝ) (hF_meas : ∀ n, AEStronglyMeasurable (F n) (μ.restrict (Ι a b)))