intervalIntegrable_log_sin — Mathlib

English

Special case of MeromorphicOn.intervalIntegrable_log: the function log ∘ sin is interval-integrable on every interval.

Русский

Особый случай: функция log ∘ sin интегрируема по мере на любой интервал.

LaTeX

$$$\text{IntervalIntegrable}(\log (\sin x))\ \text{volume}\ a\ b$$$

Lean4

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

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