English
Let 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 ∉ { z : |z−c| = |R| }.
Русский
Пусть c,w ∈ ℂ, R ∈ ℝ, n ∈ ℤ. Функция z ↦ (z−w)^n кругово интегрируема на окружности с центром c и радиусом |R| тогда и только тогда, когда R = 0 или n ≥ 0 или w не принадлежит этой окружности.
LaTeX
$$$CircleIntegrable(z\\mapsto (z-w)^n\\, , c, R) \\iff R=0 \\lor 0\\le n \\lor w\\notin sphere\\;c\\;|R|$$$
Lean4
/-- The function `fun z ↦ (z - w) ^ n`, `n : ℤ`, is circle integrable on the circle with center `c`
and radius `|R|` if and only if `R = 0` or `0 ≤ n`, or `w` does not belong to this circle. -/
@[simp]
theorem circleIntegrable_sub_zpow_iff {c w : ℂ} {R : ℝ} {n : ℤ} :
CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| :=
by
constructor
· intro h; contrapose! h; rcases h with ⟨hR, hn, hw⟩
simp only [circleIntegrable_iff R, deriv_circleMap]
rw [← image_circleMap_Ioc] at hw; rcases hw with ⟨θ, hθ, rfl⟩
replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ
set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} :=
by
suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE (deriv_circleMap_ne_zero hR)).eventually this
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
simp_all [dist_eq, sub_eq_zero]
refine
(((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
(this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans
?_
refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)
set x := ‖f θ'‖
suffices x⁻¹ ≤ x ^ n by
simp only [Algebra.id.smul_eq_mul, norm_mul, norm_inv, norm_I, mul_one]
simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff, inv_mul_cancel_left₀] using
this
have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using hθ'
rw [← zpow_neg_one]
refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_); exact hn
· rintro (rfl | H)
exacts [circleIntegrable_zero_radius,
((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
H.symm.imp_left fun (hw : w ∉ sphere c |R|) => sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']
