integral_comp_div_sub — Mathlib

English

Affine integration rules combine both addition and multiplication: ∫_a^b f(d + c x) dx = c⁻¹ ∫_{d + c a}^{d + c b} f(x) dx, Ne(c, 0).

Русский

Правила интегрирования с аффинной подстановкой: ∫_a^b f(d + c x) dx = c⁻¹ ∫_{d + c a}^{d + c b} f(x) dx, c ≠ 0.

LaTeX

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

Lean4

@[simp]
theorem integral_comp_div_sub (hc : c ≠ 0) (d) : (∫ x in a..b, f (x / c - d)) = c • ∫ x in a / c - d..b / c - d, f x :=
  by simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_sub f (inv_ne_zero hc) d

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