intervalIntegrable_log_cos — Mathlib

English

For any function f meromorphic on a compact interval, the composed log ∘ f is interval-integrable over that interval.

Русский

Для любой функции f мероморфной на компактном интервале композиция log ∘ f интегрируема по мере на этом интервале.

LaTeX

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

Lean4

/-- Special case of `MeromorphicOn.intervalIntegrable_log`: The function `log ∘ cos` is interval
integrable over every interval.
-/
theorem intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume a b :=
  analyticOnNhd_cos.meromorphicOn.intervalIntegrable_log

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