circleIntegrable_log_norm_sub_const

English

For all a,c ∈ ℂ and r ∈ ℝ, the function z ↦ log ||z − a|| is circle-integrable on the circle centered at c with radius r.

Русский

Пусть a,c ∈ ℂ и r ∈ ℝ. Функция z ↦ log ||z − a|| круговая интегрируема на окружности с центром в c и радиусом r.

LaTeX

$$$$\forall a,c\in\mathbb{C},\ \forall r\in\mathbb{R},\ CircleIntegrable(\log \|\cdot - a\|)\ c\ r.$$$$

Lean4

/-- If `a` is any complex number, the function `(log ‖· - a‖)` is circle integrable over every circle.
-/
theorem circleIntegrable_log_norm_sub_const (r : ℝ) : CircleIntegrable (log ‖· - a‖) c r :=
  circleIntegrable_log_norm_meromorphicOn (fun z hz ↦ by fun_prop)

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