integral_domSMul — Mathlib

English

For a group action on the domain, the integral of f against g•μ equals the integral of f evaluated at the transformed argument.

Русский

Для группового действия над областью интеграл от f против g•μ равен интегралу от f, вычисленному на преобразованном аргументе.

LaTeX

$$$$\int x, f(x) \partial g \cdot \mu = \int x, f((\mathrm{DomMulAct.mk}.\mathrm{symm} g)^{-1} \cdot x) \partial\mu.$$$$

Lean4

theorem integral_domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSpace A]
    [MeasurableConstSMul G A] {μ : Measure A} (g : Gᵈᵐᵃ) (f : A → E) :
    ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ :=
  integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f

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