integral_comp_neg_Ioi — Mathlib

English

A reflection identity: the integral of f(−x) over (c, ∞) equals the integral of f(x) over (−∞, −c).

Русский

Идентичность отражения: интеграл f(−x) по (c, ∞) равен интегралу f(x) по (−∞, −c).

LaTeX

$$$\int_{(c, \infty)} f(-x) \, dx = \int_{(-\infty, -c)} f(x) \, dx$$$

Lean4

@[simp]
theorem integral_comp_neg_Ioi {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (f : ℝ → E) :
    (∫ x in Ioi c, f (-x)) = ∫ x in Iic (-c), f x :=
  by
  rw [← neg_neg c, ← integral_comp_neg_Iic]
  simp only [neg_neg]

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