English
For circle-integrable f and w inside the disk, the infinite sum of the coefficients of the Cauchy power series equals the Cauchy integral with a shifted center: the w-shifted integral on the right-hand side.
Русский
Для circleIntegrable f и w внутри диска бесконечная сумма коэффициентов ряда Коши расходится в контурном интеграле со смещенным центром.
LaTeX
$$$$ HasSum\\left( n \\mapsto\\oint_{|z-c|=R} \\left( \\frac{w}{z-c} \\right)^n \\frac{1}{z-c} f(z) \\,dz \\right) = \\oint_{|z-c|=R} (z-(c+w))^{-1} f(z) \\,dz. $$$$
Lean4
theorem continuous_circleTransform {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f <| sphere z R)
(hw : w ∈ ball z R) : Continuous (circleTransform R z w f) :=
by
apply_rules [Continuous.smul, continuous_const]
· rw [funext <| deriv_circleMap _ _]
apply_rules [Continuous.mul, continuous_circleMap 0 R, continuous_const]
· exact continuous_circleMap_inv hw
· apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)
exact fun _ => (circleMap_mem_sphere _ hR.le) _
