circleTransformDeriv — Mathlib

English

The derivative of circleTransform with respect to w is given by a similar expression with (z-c)^{-1} replaced by (z-c)^{-2} and f(z) inserted at circleMap(z,R).

Русский

Производная circleTransform по переменной w имеет вид аналогичный, но с (z-c)^{-2} вместо (z-c)^{-1} и с f(z) внутри circleMap(z,R).

LaTeX

$$$$ \\text{circleTransformDeriv}(f)(\\theta) = (2\\pi i)^{-1} \\cdot \\mathrm{deriv}(\\mathrm{circleMap}\\ zR)(\\theta) \\cdot (\\mathrm{circleMap}(\\theta) - w)^{2}^{-1} \\cdot f(\\mathrm{circleMap}(\\theta)). $$$$

Lean4

/-- The derivative of `circleTransform` w.r.t. `w`. -/
def circleTransformDeriv (f : ℂ → E) (θ : ℝ) : E :=
  (2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ - w) ^ 2)⁻¹ • f (circleMap z R θ)

Похожие утверждения