English
For c,w ∈ ℂ, R ∈ ℝ, and n ∈ ℤ, the function z ↦ (z−w)^n is circle-integrable on the circle with center c and radius R if and only if R = 0 or n ≥ 0 or w ∉ sphere c|R|.
Русский
Для c,w ∈ ℂ, R ∈ ℝ и n ∈ ℤ функция z ↦ (z−w)^n кругово интегрируема на окружности с центром c и радиусом R тогда и только тогда, когда R = 0 или n ≥ 0 или w не принадлежит сфере c|R|.
LaTeX
$$$CircleIntegrable( z\\mapsto (z-w)^n, c, R) \\iff R=0 \\lor 0 \\le n \\lor w \\notin sphere c |R|$$$
Lean4
/-- Circle integrals are invariant when functions change along discrete sets. -/
theorem circleIntegral_congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℂ}
(hf : f₁ =ᶠ[codiscreteWithin (Metric.sphere c |R|)] f₂) (hR : R ≠ 0) :
(∮ z in C(c, R), f₁ z) = (∮ z in C(c, R), f₂ z) :=
by
apply intervalIntegral.integral_congr_ae_restrict
apply ae_restrict_le_codiscreteWithin measurableSet_uIoc
simp only [deriv_circleMap, smul_eq_mul, mul_eq_mul_left_iff, mul_eq_zero, circleMap_eq_center_iff, hR,
Complex.I_ne_zero, or_self, or_false]
exact codiscreteWithin.mono (by tauto) (circleMap_preimage_codiscrete hR hf)
