intervalIntegrable_log — Mathlib

English

If f is a real-valued function meromorphic on a compact interval [[a,b]], then log ||f·|| is interval-integrable on [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 _root_.MeromorphicOn.intervalIntegrable_log {f : ℝ → ℝ} (hf : MeromorphicOn f [[a, b]]) :
    IntervalIntegrable (log ∘ f) volume a b :=
  by
  rw [(by aesop : log ∘ f = (log ‖f ·‖))]
  exact intervalIntegrable_log_norm_meromorphicOn hf

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