integral_comp_smul_of_nonneg — Mathlib

English

The map of an additive Haar measure under a linear equivalence e is again Haar.

Русский

Образ меры Хаара под линейным эквивалентом остаётся мерой Хаара.

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_smul_of_nonneg (f : E → F) (R : ℝ) {hR : 0 ≤ R} :
    ∫ x, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ x, f x ∂μ := by
  rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]

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