English
For an invariant measure μ with respect to inversion on G, the Lebesgue integral satisfies ∫ f(x^{-1}) dμ = ∫ f(x) dμ for any f: G → ℝ≥0∞.
Русский
Для меры μ, инвариантной относительно инверсии на группе G, интеграл Лебега выполняется: ∫ f(x^{-1}) dμ = ∫ f(x) dμ.
LaTeX
$$$$ \\int_G f(x^{-1}) \\, d\\mu(x) = \\int_G f(x) \\, d\\mu(x). $$$$
Lean4
/-- The Lebesgue integral of a function with respect to an inverse invariant measure is
invariant under the change of variables x ↦ x⁻¹. -/
@[to_additive /-- The Lebesgue integral of a function with respect to an inverse invariant measure is
invariant under the change of variables x ↦ -x. -/
]
theorem lintegral_inv_eq_self [IsInvInvariant μ] (f : G → ℝ≥0∞) : ∫⁻ x, f x⁻¹ ∂μ = ∫⁻ x, f x ∂μ := by
simpa using (lintegral_map_equiv f (μ := μ) <| MeasurableEquiv.inv G).symm
