mulEquivHaarChar_smul_integral_map

English

For a Haar measure μ and φ, and any f, mulEquivHaarChar φ • ∫ f d(μ.map φ) = ∫ f dμ.

Русский

Для μ и φ, и любой функции f: mulEquivHaarChar φ • ∫ f d(μ.map φ) = ∫ f dμ.

LaTeX

$$$mulEquivHaarChar(\phi) \cdot \int f \; d(μ.map φ) = \int f \; dμ$$$

Lean4

@[to_additive addEquivAddHaarChar_smul_integral_map]
theorem mulEquivHaarChar_smul_integral_map (μ : Measure G) [IsHaarMeasure μ] [Regular μ] {f : G → ℝ} (φ : G ≃ₜ* G) :
    mulEquivHaarChar φ • ∫ a, f a ∂(μ.map φ) = ∫ a, f a ∂μ :=
  by
  nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
  simp

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