integral_comp_add_mul — Mathlib

English

For any measurable f with appropriate integrability on [a,b] and nonzero c, the integral of f on the affine image d+c x over [a,b] equals c^{-1} times the integral of f on the interval [d+ca, d+cb].

Русский

Для измеримой функции f, интегрируемой на отрезке [a,b], при ненулевом c выполняется формула замены переменной: ∫_a^b f(d+cx) dx = c^{-1} ∫_{d+ca}^{d+cb} f(x) dx.

LaTeX

$$$c \\neq 0 \\Rightarrow \\int_{a}^{b} f(d+c x)\\,dx = c^{-1} \\int_{d+c a}^{d+c b} f(x)\\,dx.$$$

Lean4

@[simp]
theorem integral_comp_add_mul (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (d + c * x)) = c⁻¹ • ∫ x in d + c * a..d + c * b, f x := by
  rw [← integral_comp_add_left, ← integral_comp_mul_left _ hc]

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