English
Let E be a normed space. For a function f from the complex plane to E, the circle average circleAverage(f, c, R) is the average value of f on the circle with center c and radius R, parameterized by circleMap c R θ for θ in [0, 2π].
Русский
Пусть E обладает нормированным размещением. Для функции f: ℂ → E среднее по окружности circleAverage(f, c, R) задаёт среднее значение функции на окружности с центром в c и радиусом R, параметризованной circleMap c R θ по θ ∈ [0, 2π].
LaTeX
$$$circleAverage\ f\ c\ R = \dfrac{1}{2\pi}\int_{0}^{2\pi} f\big(circleMap\ c\ R\ \theta\big)\,d\theta$$$
Lean4
/-- Define `circleAverage f c R` as the average value of `f` on the circle with center `c` and radius
`R`. This is a real notion, which should not be confused with the complex path integral notion
defined in `circleIntegral` (integrating with respect to `dz`).
-/
noncomputable def circleAverage : E :=
(2 * π)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ)
