circleIntegrable_log_norm_factorizedRational

English

Variant of MeromorphicOn.intervalIntegrable_log for a sum of logs of linear factors; the circle integral of such a finite factorization is integrable.

Русский

Вариант: сумма логарифмов линейных множителей рациональной функции; окружностная интегрируемость сохраняется.

LaTeX

$$$\text{CircleIntegrable}\left(\sum_{u} (D(u) \cdot \log \|\cdot - u\|)\right)\ c\ R$$$

Lean4

/-- Variant of `circleIntegrable_log_norm_meromorphicOn` for factorized rational functions.
-/
theorem circleIntegrable_log_norm_factorizedRational {R : ℝ} {c : ℂ} (D : ℂ → ℤ) :
    CircleIntegrable (∑ᶠ u, ((D u) * log ‖· - u‖)) c R :=
  CircleIntegrable.finsum
    (fun _ ↦
      (circleIntegrable_log_norm_meromorphicOn (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn).const_smul)

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