integral_inv_eq_self — Mathlib

English

If μ is invariant under inversion, then the integral of a function f equals the integral of f composed with inversion.

Русский

Если мера инвариантна относительно обращения, то интеграл функции f равен интегралу функции f, композиционной с обращением.

LaTeX

$$$\\int_G f(x)\\,dμ(x) = \\int_G f(x^{-1})\\,dμ(x)$ when μ is inversion-invariant.$$

Lean4

@[to_additive]
theorem integral_inv_eq_self (f : G → E) (μ : Measure G) [IsInvInvariant μ] : ∫ x, f x⁻¹ ∂μ = ∫ x, f x ∂μ :=
  by
  have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
  rw [← h.integral_map, map_inv_eq_self]

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