integral_smul_eq_self — Mathlib

English

If f is integrable with respect to μ ∗ₘ ν, then the integral of f over the convolution equals the iterated integral of f over ν and then μ, i.e., ∫ f d(μ ∗ₘ ν) = ∫ ∫ f(xy) dν(y) dμ(x).

Русский

Если f интегрируема по мере μ ∗ₘ ν, то интеграл по объединённой (свёртке) мере равен повторному интегралу: ∫ f(xy) dν(y) dμ(x).

LaTeX

$$$$ \\int_G f(x) \\, d(\\mu \\ast_m \\nu)(x) = \\int_G \\int_G f(xy) \\, d\\nu(y) \\, d\\mu(x). $$$$

Lean4

@[to_additive]
theorem integral_smul_eq_self {μ : Measure α} [SMulInvariantMeasure G α μ] (f : α → E) {g : G} :
    (∫ x, f (g • x) ∂μ) = ∫ x, f x ∂μ :=
  by
  have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
  rw [← h.integral_map, MeasureTheory.map_smul]

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