Theorems · Theorem · measure theory

MeasureTheory.integral_eq_zero_of_mul_left_eq_neg

∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulLeftInvariant],
  (∀ (x : G), f (g * x) = -f x) → ∫ (x : G), f x ∂μ = 0

If some left-translate of a function negates it, then the integral of the function with respect to a left-invariant measure is 0.

Defined in

Mathlib.MeasureTheory.Group.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceGroupMeasurableMulMeasureTheory.Measure.IsMulLeftInvariant