English
If μ is left-invariant and ν is left-invariant, then their product measure μ × ν is left-invariant.
Русский
Если μ и ν — левая инвариантность, то их произведение (плотность) μ·ν также сохраняет левую инвариантность.
LaTeX
$$$\text{IsMulLeftInvariant}(μ) \land \text{IsMulLeftInvariant}(ν) \Rightarrow \text{IsMulLeftInvariant}(μ\,\mathrm{prod}\,ν)$$$
Lean4
/-- An alternative way to prove that `μ` is right invariant under multiplication. -/
@[to_additive /-- An alternative way to prove that `μ` is right invariant under addition. -/
]
theorem forall_measure_preimage_mul_right_iff (μ : Measure G) :
(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔ IsMulRightInvariant μ :=
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_mul_const g) hA]
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩
