English
Let G act distributively on A with Haar measures. There exists a unique monoid hom Δ: G → ℝ≥0 such that for every Haar measure μ on A and every measurable set S ⊆ A, μ(g • S) = Δ(g) μ(S).
Русский
Пусть G действует на A распределённо и существует мера Хаара μ на A. Существует единственный моноид-гомоморфизм Δ: G → ℝ≥0 такой, что для любой меры Хаара μ и любого измеримого множества S ⊆ A выполняется μ(g • S) = Δ(g) μ(S).
LaTeX
$$$\\Delta: G \\to \\mathbb{R}_{\\ge 0}$ является моноид-гомоморфизмом и для любой меры Хаара $\\mu$ на $A$ и любого измеримого множества $S \\subseteq A$ выполняется $\\mu(g\\cdot S)=\\Delta(g)\\,\\mu(S)$.$$
Lean4
/-- The distributive Haar character of a group `G` acting distributively on a group `A` is the
unique positive real number `Δ(g)` such that `μ (g • s) = Δ(g) * μ s` for all Haar
measures `μ : Measure A`, set `s : Set A` and `g : G`. -/
@[simps -isSimp]
noncomputable def distribHaarChar : G →* ℝ≥0 :=
letI := borel A
haveI : BorelSpace A := ⟨rfl⟩
{ toFun g := addHaarScalarFactor (DomMulAct.mk g • addHaar) (addHaar (G := A))
map_one' := by simp
map_mul' g
g' := by
simp_rw [DomMulAct.mk_mul]
rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]
congr 1
simp_rw [mul_smul]
rw [addHaarScalarFactor_domSMul] }
