English
For a measure μ on a group G with measurable multiplication, μ is left-invariant iff for every g ∈ G and every measurable set A, μ((g·)^{-1}A) = μ(A).
Русский
Для меры μ на группе G с измеримой операцией умножения μ есть левое инвариантное тогда и только тогда, когда для каждого элемента g группы и каждого измеримого множества A выполняется μ((g·)^{-1}A) = μ(A).
LaTeX
$$$\Bigl( \forall g\in G, \forall A,\ MeasurableSet(A)\Rightarrow μ((g\cdot)^{-1}A)=μ(A)\Bigr)\ \Longleftrightarrow\ IsMulLeftInvariant μ.$$
Lean4
/-- An alternative way to prove that `μ` is left invariant under multiplication. -/
@[to_additive /-- An alternative way to prove that `μ` is left invariant under addition. -/
]
theorem forall_measure_preimage_mul_iff (μ : Measure G) :
(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔ IsMulLeftInvariant μ :=
by
trans ∀ g, map (g * ·) μ = μ
· simp_rw [Measure.ext_iff]
refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_
rw [map_apply (measurable_const_mul g) hA]
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩
