circleIntegrable_sub_inv_iff — Mathlib

English

Let c,w ∈ ℂ and R ∈ ℝ. The function z ↦ (z−w)^{-1} is circle-integrable on the circle centered at c with radius R if and only if R = 0 or w ∉ { z : |z−c| = |R| }.

Русский

Пусть c,w ∈ ℂ и R ∈ ℝ. Функция z ↦ (z−w)^{-1} кругово интегрируема вдоль окружности с центром в c и радиусом R тогда и только тогда, когда R = 0 или w не лежит на этой окружности.

LaTeX

$$$CircleIntegrable\\bigl( z\\mapsto (z-w)^{-1}, c, R \\bigr) \\iff R=0 \\lor w\\notin sphere\\;c\\;|R|$$$

Lean4

@[simp]
theorem circleIntegrable_sub_inv_iff {c w : ℂ} {R : ℝ} :
    CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ sphere c |R| := by
  simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]; simp

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