continuous_circleTransformDeriv — Mathlib

English

For circle-integrable f and w with |w|<R, the sum over n of the coefficients of the Cauchy power series equals the Cauchy integral with center c shifted by w, up to the (2πi)^{-1} factor.

Русский

Для circleIntegrable f и w с |w|<R сумма коэффициентов ряда Коши равна соответствующему контурному интегралу с центром смещенным на w, умноженным на (2πi)^{-1}.

LaTeX

$$$$ HasSum\\left( n \\mapsto \\text{coefficient}_n\\right) = (2\\pi i)^{-1} \\oint_{z\\in C(c,R)} (z-(c+w))^{-1} f(z) \\,dz. $$$$

Lean4

theorem continuous_circleTransformDeriv {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (sphere z R))
    (hw : w ∈ ball z R) : Continuous (circleTransformDeriv R z w f) :=
  by
  rw [circleTransformDeriv_eq]
  exact (continuous_circleMap_inv hw).smul (continuous_circleTransform hR hf hw)

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