circleTransformDeriv_eq — Mathlib

English

The integral over θ of circleTransform equals a scaled circle integral with shifted center: ∫ circleTransform dθ = (2πi)^{-1} ∮ (z-w)^{-1} f(z) dz.

Русский

Интеграл по θ от circleTransform равен нормированному константному множителю контурному интегралу с центр смещён на w.

LaTeX

$$$$ \\int_{0}^{2\\pi} \\text{circleTransform}(f)(\\theta)\\, d\\theta = (2\\pi i)^{-1} \\oint_{|z-c|=R} (z-w)^{-1} f(z) \\,dz. $$$$

Lean4

theorem circleTransformDeriv_eq (f : ℂ → E) :
    circleTransformDeriv R z w f = fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ :=
  by
  ext
  simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]
  ring_nf
  rw [inv_pow]
  congr
  ring

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