lintegral_div_right_eq_self — Mathlib

English

If μ is right-invariant, then for any g the equality ∫ f(x/g) dμ(x) = ∫ f(x) dμ(x) holds for f: G → ℝ≥0∞.

Русский

Если μ — правая инвариантная, то ∫ f(x/g) dμ(x) = ∫ f(x) dμ(x).

LaTeX

$$$$ \\int_G f(x/g) \\, d\\mu(x) = \\int_G f(x) \\, d\\mu(x). $$$$

Lean4

@[to_additive]
theorem lintegral_div_right_eq_self [IsMulRightInvariant μ] (f : G → ℝ≥0∞) (g : G) :
    (∫⁻ x, f (x / g) ∂μ) = ∫⁻ x, f x ∂μ := by simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]

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