integral_comp_inv_smul_of_nonneg — Mathlib

English

Properties about continuity of measure maps with respect to linear maps and Haar measures.

Русский

Свойства непрерывности отображений мер при линейных отображениях и мера Хаара.

LaTeX

$$$$(μ.map e).IsAddHaarMeasure$$$$

Lean4

/-- The integral of `f (R⁻¹ • x)` with respect to an additive Haar measure is a multiple of the
integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
thanks to the convention that a non-integrable function has integral zero. -/
theorem integral_comp_inv_smul_of_nonneg (f : E → F) {R : ℝ} (hR : 0 ≤ R) :
    ∫ x, f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ x, f x ∂μ := by
  rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]

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