intervalIntegrable_posLog_norm_meromorphicOn

English

If f is meromorphic on the compact interval [[a,b]], then log ||f|| is interval-integrable over [a,b].

Русский

Если функция f мероморфна на компактном интервале [[a,b]], то log ||f|| интегрируема по мере на отрезке [a,b].

LaTeX

$$$\text{IntervalIntegrable}(\log \|f\|)\ \text{volume}\ a\ b$$$

Lean4

/-- If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
-/
theorem intervalIntegrable_posLog_norm_meromorphicOn (hf : MeromorphicOn f [[a, b]]) :
    IntervalIntegrable (log⁺ ‖f ·‖) volume a b :=
  by
  simp_rw [← half_mul_log_add_log_abs, mul_add]
  apply IntervalIntegrable.add
  · apply (intervalIntegrable_log_norm_meromorphicOn hf).const_mul
  · apply (intervalIntegrable_log_norm_meromorphicOn hf).abs.const_mul

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