inv_mul_integral_comp_add_div — Mathlib

English

Variant of circle integrability for nonnegative radius; the same as MeromorphicOn.intervalIntegrable_log.

Русский

Вариант неотрицательного радиуса: логарифм норм мероморфной функции интегрируем на окружности.

LaTeX

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

Lean4

@[simp]
theorem inv_mul_integral_comp_add_div : (c⁻¹ * ∫ x in a..b, f (d + x / c)) = ∫ x in d + a / c..d + b / c, f x :=
  inv_smul_integral_comp_add_div f c d

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