circleIntegrable_log_norm_meromorphicOn_of_nonneg

English

If f is meromorphic on a circle sphere c|R|, then log ‖f‖ is circle-integrable on that circle.

Русский

Если f мероморфна на окружности сферы c|R|, то log ‖f‖ интегрируема по окружности на этой окружности.

LaTeX

$$$\text{CircleIntegrable}(\log \|f\|)\ c\ R$$$

Lean4

/-- Variant of `circleIntegrable_log_norm_meromorphicOn` for non-negative radii.
-/
theorem circleIntegrable_log_norm_meromorphicOn_of_nonneg (hf : MeromorphicOn f (sphere c R)) (hR : 0 ≤ R) :
    CircleIntegrable (log ‖f ·‖) c R := by
  rw [← abs_of_nonneg hR] at hf
  exact circleIntegrable_log_norm_meromorphicOn hf

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