smul_integral_comp_mul_add — Mathlib

English

For any f, the smoothed integral identity with both additive and multiplicative affine transformation holds: ∫_a^b f(d + c x) dx = c⁻¹ ∫_{d + c a}^{d + c b} f(x) dx.

Русский

Для любых f выполняется формула со смешанным аффинным преобразованием: ∫_a^b f(d + c x) dx = c⁻¹ ∫_{d + c a}^{d + c b} f(x) dx.

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 smul_integral_comp_mul_add (c d) : (c • ∫ x in a..b, f (c * x + d)) = ∫ x in c * a + d..c * b + d, f x := by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_add]

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