integral_div_left_eq_self — Mathlib

English

For a left-invariant and invertible measure μ on a group G, and any g ∈ G, the integral of f(g/x) over x with respect to μ equals the integral of f(x) over x with respect to μ.

Русский

При возм. слева и инверсии меры μ на группе G, для любого g ∈ G имеет место равенство: ∫ f(g/x) dμ = ∫ f(x) dμ.

LaTeX

$$$$ \\int_G f\\left(\\frac{g}{x}\\right) \\, d\\mu(x) = \\int_G f(x) \\, d\\mu(x). $$$$

Lean4

@[to_additive]
theorem integral_div_left_eq_self (f : G → E) (μ : Measure G) [IsInvInvariant μ] [IsMulLeftInvariant μ] (x' : G) :
    (∫ x, f (x' / x) ∂μ) = ∫ x, f x ∂μ := by
  simp_rw [div_eq_mul_inv, integral_inv_eq_self (fun x => f (x' * x)) μ, integral_mul_left_eq_self f x']

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