English
If R ≠ 0, circleAverage equals the appropriately scaled contour integral over the circle |z−c|=R of (z−c)^{-1} f(z).
Русский
Если R ≠ 0, circleAverage равняется надлежащим образом нормированному контурному интегралу по окружности |z−c|=R от (z−c)^{-1} f(z).
LaTeX
$$$circleAverage\ f\ c\ R = (2\pi i)^{-1} \oint_{|z-c|=R} (z-c)^{-1} f(z)\,dz$$$
Lean4
/-- Expression of the `circleAverage` in terms of a `circleIntegral`.
-/
theorem circleAverage_eq_circleIntegral {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (h : R ≠ 0) :
circleAverage f c R = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
calc
circleAverage f c R
_ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by simp [circleAverage, ← coe_smul]
_ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) :=
by
rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
match_scalars
field_simp
_ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) :=
by
unfold circleIntegral
congr with θ
simp [deriv_circleMap, circleMap_sub_center, smul_smul]
field_simp [circleMap_ne_center h]
