circleIntegrable_posLog_norm_meromorphicOn

English

If f is meromorphic on [[a,b]], then log⁺ ‖f‖ is circle-integrable on that circle.

Русский

Если f мероморфна на кольце, то log⁺ ‖f‖ интегрируема по мере на этом круге.

LaTeX

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

Lean4

/-- If `f` is complex meromorphic on a circle in the complex plane, then `log⁺ ‖f ·‖` is circle
integrable over that circle.
-/
theorem circleIntegrable_posLog_norm_meromorphicOn (hf : MeromorphicOn f (sphere c |R|)) :
    CircleIntegrable (log⁺ ‖f ·‖) c R :=
  by
  simp_rw [← half_mul_log_add_log_abs, mul_add]
  apply CircleIntegrable.add
  · apply (circleIntegrable_log_norm_meromorphicOn hf).const_mul
  · apply (circleIntegrable_log_norm_meromorphicOn hf).abs.const_mul

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