English
Let g: ℝ → E and a ∈ ℝ with b > 0. Then ∫_{x > a} g(bx) dx = b^{-1} ∫_{x > ab} g(x) dx, i.e., a change of variables by scaling on the left.
Русский
Пусть g: ℝ → E, a ∈ ℝ и b > 0. Тогда ∫_{x > a} g(bx) dx = b^{-1} ∫_{x > ab} g(x) dx, т. е. заменa переменной через масштаб слева.
LaTeX
$$$$ \int_{x \in Ioi a} g(bx) \, dx = b^{-1} \; \int_{x \in Ioi (ba)} g(x) \, dx, \quad b > 0. $$$$
Lean4
theorem integral_comp_mul_left_Ioi (g : ℝ → E) (a : ℝ) {b : ℝ} (hb : 0 < b) :
(∫ x in Ioi a, g (b * x)) = b⁻¹ • ∫ x in Ioi (b * a), g x :=
by
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
rw [← integral_indicator (this a), ← integral_indicator (this (b * a)), ← abs_of_pos (inv_pos.mpr hb), ←
Measure.integral_comp_mul_left]
congr
ext1 x
rw [← indicator_comp_right, preimage_const_mul_Ioi _ hb, mul_div_cancel_left₀ _ hb.ne', Function.comp_def]
