smul_integral_comp_mul_sub — Mathlib

English

With subtraction of the interval, we have: ∫_a^b f(x - d) dx = ∫_{a - d}^{b - d} f(x) dx.

Русский

Сдвиг и вычитание аргумента: ∫_a^b f(x - d) dx = ∫_{a - d}^{b - d} f(x) dx.

LaTeX

$$$$\int_{a}^{b} f(x - d) \, dx = \int_{a - d}^{b - d} f(x) \, dx.$$$$

Lean4

@[simp]
theorem smul_integral_comp_mul_sub (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_sub]

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