feat: simple lemmas on circle integrability (#39566)

Add several very simple but useful lemmas on circle integrability and circle averages.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), formalizing Value Distribution Theory for meromorphic functions on the complex plane.

Author: kebekus

Mathlib/MeasureTheory/Integral/CircleAverage.lean

@@ -209,6 +209,15 @@ theorem ContinuousOn.circleAverage {f : ℂ → E} {s : Set ℝ} {c : ℂ}
   apply hf.comp (f := (fun x ↦ ⟨circleMap c x.1 x.2, this x⟩))
   fun_prop
 
+/--
+The circle average of a continuous function is itself continuous, as a function
+of the radius.
+-/
+@[fun_prop] theorem Continuous.circleAverage {f : ℂ → E} (hf : Continuous f) :
+    Continuous (Real.circleAverage f c) := by
+  apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul
+  fun_prop
+
 /--
 Companion lemma to `ContinuousOn.circleAverage`: a function continuous on `Ioc r
 R` and constant on `Ioo r R` is constant.

Mathlib/MeasureTheory/Integral/CircleIntegral.lean

@@ -194,9 +194,13 @@ Analogue of `IntervalIntegrable.abs`: If a real-valued function `f` is circle in
 theorem abs {f : ℂ → ℝ} (hf : CircleIntegrable f c R) :
     CircleIntegrable |f| c R := IntervalIntegrable.abs hf
 
-nonrec theorem add (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) :
+@[to_fun] theorem add (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) :
     CircleIntegrable (f + g) c R :=
-  hf.add hg
+  IntervalIntegrable.add hf hg
+
+@[to_fun] theorem sub (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) :
+    CircleIntegrable (f - g) c R :=
+  IntervalIntegrable.sub hf hg
 
 /-- Sums of circle integrable functions are circle integrable. -/
 protected theorem sum {ι : Type*} (s : Finset ι) {f : ι → ℂ → E}
@@ -233,6 +237,29 @@ theorem const_smul {f : ℂ → A} (h : CircleIntegrable f c R) : CircleIntegrab
 theorem const_fun_smul {f : ℂ → A} (h : CircleIntegrable f c R) :
     CircleIntegrable (fun z ↦ a • f z) c R := const_smul h
 
+variable
+  {𝕜 F : Type*} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F]
+
+/--
+If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g • f` is
+circle integrable.
+-/
+@[to_fun] theorem smul_of_continuousOn {f : ℂ → F} {g : ℂ → 𝕜} (hf : CircleIntegrable f c R)
+    (hg : ContinuousOn g (sphere c |R|)) :
+    CircleIntegrable (g • f) c R :=
+  IntervalIntegrable.continuousOn_smul hf
+    (hg.comp (by fun_prop) (fun x hx ↦ circleMap_mem_sphere' c R x))
+
+/--
+If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g * f` is
+circle integrable.
+-/
+@[to_fun] theorem mul_of_continuousOn {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R)
+    (hg : ContinuousOn g (sphere c |R|)) :
+    CircleIntegrable (g * f) c R :=
+  IntervalIntegrable.continuousOn_mul hf
+    (hg.comp (by fun_prop) (fun x hx ↦ circleMap_mem_sphere' c R x))
+
 /-- The function we actually integrate over `[0, 2π]` in the definition of `circleIntegral` is
 integrable. -/
 theorem out [NormedSpace ℂ E] (hf : CircleIntegrable f c R) :