integral_eq_zero_of_mul_right_eq_neg

English

The integral of a function is unchanged by applying the inversion map on the group when μ is invariant under inversion.

Русский

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

LaTeX

$$$\\int_G f(x) dμ(x) = \\int_G f(x^{-1}) dμ(x)$ for IsInvInvariant μ.$$

Lean4

/-- If some right-translate of a function negates it, then the integral of the function with respect
to a right-invariant measure is 0. -/
@[to_additive /-- If some right-translate of a function negates it, then the integral of the function with
          respect to a right-invariant measure is 0. -/
    ]
theorem integral_eq_zero_of_mul_right_eq_neg [IsMulRightInvariant μ] (hf' : ∀ x, f (x * g) = -f x) : ∫ x, f x ∂μ = 0 :=
  by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]

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