integral_comp_add_right — Mathlib

English

Let a, b, c > 0 with c ≠ 0. Then the integral of f(x / c) over [a, b] equals c times the integral over [a/c, b/c]. More precisely, ∫_a^b f(x / c) dx = c • ∫_{a/c}^{b/c} f(x) dx.

Русский

Пусть c ≠ 0. Тогда ∫_a^b f(x / c) dx = c • ∫_{a/c}^{b/c} f(x) dx.

LaTeX

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

Lean4

@[simp]
theorem integral_comp_add_right (d) : (∫ x in a..b, f (x + d)) = ∫ x in a + d..b + d, f x :=
  have A : MeasurableEmbedding fun x => x + d := (Homeomorph.addRight d).isClosedEmbedding.measurableEmbedding
  calc
    (∫ x in a..b, f (x + d)) = ∫ x in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume := by
      simp [intervalIntegral, A.setIntegral_map]
    _ = ∫ x in a + d..b + d, f x := by rw [map_add_right_eq_self]

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