English
For a nonzero constant c, the integral of f(x·c) over [a, b] equals c⁻¹ times the integral of f over [a·c, b·c]. Precisely, ∫_a^b f(x c) dx = c⁻¹ ∫_{a c}^{b c} f(u) du when c ≠ 0.
Русский
При ненулевой константе c выполняется подстановочная формула замены переменной: ∫_a^b f(x c) dx = c⁻¹ ∫_{a c}^{b c} f(u) du, если c ≠ 0.
LaTeX
$$$$\int_{a}^{b} f(x c) \, dx = c^{-1} \int_{a c}^{b c} f(u) \, du \quad (c \neq 0).$$$$
Lean4
@[simp]
theorem integral_comp_mul_right (hc : c ≠ 0) : (∫ x in a..b, f (x * c)) = c⁻¹ • ∫ x in a * c..b * c, f x :=
by
have A : MeasurableEmbedding fun x => x * c := (Homeomorph.mulRight₀ c hc).isClosedEmbedding.measurableEmbedding
conv_rhs => rw [← Real.smul_map_volume_mul_right hc]
simp_rw [integral_smul_measure, intervalIntegral, A.setIntegral_map, ENNReal.toReal_ofReal (abs_nonneg c)]
rcases hc.lt_or_gt with h | h
· simp [h, mul_div_cancel_right₀, hc, abs_of_neg, Measure.restrict_congr_set (α := ℝ) (μ := volume) Ico_ae_eq_Ioc]
· simp [h, mul_div_cancel_right₀, hc, abs_of_pos]
