smul_integral_comp_sub_mul — Mathlib

English

Affine transformations with both addition and division: ∫_a^b f(d + x/c) dx = c ∙ ∫_{a/c + d}^{b/c + d} f(x) dx.

Русский

Афинная подстановка с добавлением и делением: ∫_a^b f(d + x/c) dx = c ∙ ∫_{a/c + d}^{b/c + d} f(x) dx.

LaTeX

$$$$\int_{a}^{b} f\left(d + \frac{x}{c}\right) dx = c \cdot \int_{a/c + d}^{b/c + d} f(x) \, dx.$$$$

Lean4

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

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