English
The circle transform maps θ to a scaled derivative along circleMap, multiplied by the inverse of (circleMap θ − w) and by f(circleMap θ).
Русский
Преобразование круга принимает θ в пропорциональную производную вдоль circleMap, умножает на обратное (circleMap θ − w) и на f(circleMap θ).
LaTeX
$$$$ \\text{circleTransform}(f)(\\theta) = (2\\pi i)^{-1} \\cdot \\mathrm{deriv}(\\mathrm{circleMap}\\ zR)(\\theta) \\cdot (\\mathrm{circleMap}(\\theta) - w)^{-1} \\cdot f(\\mathrm{circleMap}(\\theta)). $$$$
Lean4
/-- Given a function `f : ℂ → E`, `circleTransform R z w f` is the function mapping `θ` to
`(2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ) - w)⁻¹ • f (circleMap z R θ)`.
If `f` is differentiable and `w` is in the interior of the ball, then the integral from `0` to
`2 * π` of this gives the value `f(w)`. -/
def circleTransform (f : ℂ → E) (θ : ℝ) : E :=
(2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ)
