smul_integral_comp_mul_left — Mathlib

English

For any f, c, d, the integral of f(c x + d) over [a, b] equals c⁻¹ times the integral of f over [c a + d, c b + d]. Precisely, ∫_a^b f(c x + d) dx = c⁻¹ ∫_{c a + d}^{c b + d} f(x) dx when c ≠ 0.

Русский

Для любого f, c, d верна формула: ∫_a^b f(c x + d) dx = c⁻¹ ∫_{c a + d}^{c b + d} f(x) dx, при c ≠ 0.

LaTeX

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

Lean4

@[simp]
theorem smul_integral_comp_mul_left (c) : (c • ∫ x in a..b, f (c * x)) = ∫ x in c * a..c * b, f x := by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_left]

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