English
The circle integral of a function f: ℂ → E around a circle with center c and radius R is the integral over θ ∈ [0,2π] of deriv(circleMap c R) θ times f(circleMap c R θ).
Русский
Круговой интеграл функции f: ℂ→E вокруг окружности с центром c и радиусом R равен интегралу по параметру θ ∈ [0,2π] от производной circleMap(c,R) в точке θ, умноженной на f(circleMap(c,R) θ).
LaTeX
$$$ circleIntegral(f,c,R) := \\int_{0}^{2\\pi} \\bigl( \\ deriv(circleMap\\; c\\; R)\\; \\theta \\bigr) \\cdot f(circleMap\\; c\\; R\\; \\theta) \\, d\\theta $$$
Lean4
/-- Definition for $\oint_{|z-c|=R} f(z)\,dz$ -/
def circleIntegral (f : ℂ → E) (c : ℂ) (R : ℝ) : E :=
∫ θ : ℝ in 0..2 * π, deriv (circleMap c R) θ • f (circleMap c R θ)
