Theorems · Theorem · measure theory

MeasureTheory.lintegral_inv_eq_self

∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : InvolutiveInv G] [MeasurableInv G]
  [μ.IsInvInvariant] (f : G → ENNReal), ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

The Lebesgue integral of a function with respect to an inverse invariant measure is invariant under the change of variables x ↦ x⁻¹.

Defined in

Mathlib.MeasureTheory.Group.LIntegral

Cited by

2 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceInvolutiveInvMeasurableInvMeasureTheory.Measure.IsInvInvariant