English
Translating a function by left-multiplication does not change its integral with respect to a left-invariant measure.
Русский
Сдвиг функции слева не изменяет интеграл относительно левой инвариантной меры.
LaTeX
$$$\\int_G f(gx) dμ(x) = \\int_G f(x) dμ(x)$ under left invariance.$$
Lean4
/-- Translating a function by left-multiplication does not change its integral with respect to a
left-invariant measure. -/
@[to_additive /-- Translating a function by left-addition does not change its integral with respect to a
left-invariant measure. -/
]
theorem integral_mul_left_eq_self [IsMulLeftInvariant μ] (f : G → E) (g : G) : (∫ x, f (g * x) ∂μ) = ∫ x, f x ∂μ :=
by
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
rw [← h_mul.integral_map, map_mul_left_eq_self]
