mul_integral_comp_mul_left

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

URI: https://scilib.ai/kg/mathlib#intervalIntegral.mul_integral_comp_mul_left

English

Special case of MeromorphicOn.intervalIntegrable_log: log ∘ cos is interval-integrable over every interval.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mul_integral_comp_mul_left : (c * ∫ x in a..b, f (c * x)) = ∫ x in c * a..c * b, f x :=
  smul_integral_comp_mul_left f c

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru