integral_comp_mul_right_Ioi — Mathlib

English

Let g: ℝ → E and a ∈ ℝ with b > 0. Then ∫_{x > a} g(x b) dx = b^{-1} ∫_{x > a b} g(x) dx, i.e., a right-hand substitution.

Русский

Пусть g: ℝ → E, a ∈ ℝ и b > 0. Тогда ∫_{x > a} g(x b) dx = b^{-1} ∫_{x > a b} g(x) dx.

LaTeX

$$$$ \int_{x \in Ioi a} g(xb) \, dx = b^{-1} \int_{x \in Ioi (ab)} g(x) \, dx, \quad b > 0. $$$$

Lean4

theorem integral_comp_mul_right_Ioi (g : ℝ → E) (a : ℝ) {b : ℝ} (hb : 0 < b) :
    (∫ x in Ioi a, g (x * b)) = b⁻¹ • ∫ x in Ioi (a * b), g x := by
  simpa only [mul_comm] using integral_comp_mul_left_Ioi g a hb

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