English
For a function f: R → E, the integral over (−∞, c] of f(−x) equals the integral over (−∞, −c) of f(x) after appropriate rearrangement, i.e., a symmetry under reflection.
Русский
Для функции f: R → E интеграл по (−∞, c] от f(−x) равен интегралу по (−∞, −c) от f(x) после соответствующего преобразования, то есть симметрия по отражению.
LaTeX
$$$\int_{(-\infty,c]} f(-x) \, dx = \int_{(-\infty,-c]} f(x) \, dx$$$
Lean4
@[simp]
theorem integral_comp_neg_Iic {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (f : ℝ → E) :
(∫ x in Iic c, f (-x)) = ∫ x in Ioi (-c), f x :=
by
have A : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).isClosedEmbedding.measurableEmbedding
have := MeasurableEmbedding.setIntegral_map (μ := volume) A f (Ici (-c))
rw [Measure.map_neg_eq_self (volume : Measure ℝ)] at this
simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]
