comp_mul_left' — Mathlib

English

If g: ℝ → F is integrable, then for any nonzero R, the function x ↦ g(Rx) is integrable with the same measure (Lebesgue).

Русский

Если g: ℝ → F интегрируема, то для любого ненулевого R функция x ↦ g(Rx) интегрируема по той же мере (мера Лебега).

LaTeX

$$$\\text{Integrable}(g) \\Rightarrow \\text{Integrable}(x \\mapsto g(Rx)), \\; R \\neq 0,$ где мера — объём.$$

Lean4

theorem comp_mul_left' {g : ℝ → F} (hg : Integrable g) {R : ℝ} (hR : R ≠ 0) : Integrable fun x => g (R * x) :=
  (integrable_comp_mul_left_iff g hR).2 hg

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