Theorems · Theorem · measure theory

MeasureTheory.lintegral_neg_eq_self

∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : InvolutiveNeg G] [MeasurableNeg G]
  [μ.IsNegInvariant] (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

MeasurableSpaceInvolutiveNegMeasurableNegMeasureTheory.Measure.IsNegInvariant