English
The map (x,y) ↦ y*x is quasi-measure-preserving from μ×ν to μ under left-invariance assumptions.
Русский
Отображение (x,y)↦yx является квази-меропроизведением от μ×ν к μ при условии левой инвариантности.
LaTeX
$$$\text{QuasiMeasurePreserving}( (p_1,p_2) \mapsto p_2 p_1) (\mu \times \nu) \; \mu$$$
Lean4
/-- Left invariant Borel measures on a measurable group are unique (up to a scalar). -/
@[to_additive /-- Left invariant Borel measures on an additive measurable group are unique (up to a scalar). -/
]
theorem measure_eq_div_smul (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) : μ' = (μ' s / ν' s) • ν' :=
by
ext1 t -
rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm, measure_mul_measure_eq μ' ν' s t h2s h3s,
mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]
