addHaarScalarFactor_smul_eq_distribHaarChar

English

For a Haar measure μ on A and any g ∈ G, the scalar factor relating the pushforward of μ by g to μ is Δ(g): addHaarScalarFactor (g•μ, μ) = Δ(g).

Русский

Для меры Хаара μ на A и любого элемента g ∈ G отношение ростов массы по действию g задаётся скалярным фактором Δ(g): addHaarScalarFactor (g•μ, μ) = Δ(g).

LaTeX

$$$\\mathrm{addHaarScalarFactor} (g\\cdot \\mu, \\mu) = \\Delta(g) \\quad$ для всех $g\\in G$ и для любой меры Хаара $\\mu$ на $A$.$$

Lean4

theorem addHaarScalarFactor_smul_eq_distribHaarChar (g : G) :
    addHaarScalarFactor (DomMulAct.mk g • μ) μ = distribHaarChar A g :=
  by
  borelize A
  exact addHaarScalarFactor_smul_congr' ..

Похожие утверждения