inv_smul_integral_comp_sub_div — Mathlib

English

Let f: R → E be integrable on [a,b]. For any real c ≠ 0 and d ∈ R, we have a change of variables formula: c^{-1} ∫_a^b f(d − x/c) dx = ∫_{d − b/c}^{d − a/c} f(x) dx.

Русский

Пусть f: ℝ → E интегрируема на отрезке [a,b]. При любом c ∈ ℝ, не равном нулю, и любом d ∈ ℝ выполняется формула замены переменной: c^{-1} ∫_a^b f(d − x/c) dx = ∫_{d − b/c}^{d − a/c} f(x) dx.

LaTeX

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

Lean4

@[simp]
theorem inv_smul_integral_comp_sub_div (c d) : (c⁻¹ • ∫ x in a..b, f (d - x / c)) = ∫ x in d - b / c..d - a / c, f x :=
  by by_cases hc : c = 0 <;> simp [hc, integral_comp_sub_div]

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