setIntegral_comp_smul_of_pos — Mathlib

English

Inverse scaling: integral with R⁻¹ appears with factor |R|^finrank.

Русский

Применение обратного коэффициента масштабирования дает фактор |R|^finrank.

LaTeX

$$$\int_G f(R^{-1}x) dμ = |R|^{\mathrm{finrank}} \int_G f(x) dμ$$$

Lean4

theorem setIntegral_comp_smul_of_pos (f : E → F) {R : ℝ} (s : Set E) (hR : 0 < R) :
    ∫ x in s, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ x in R • s, f x ∂μ := by
  rw [setIntegral_comp_smul μ f s hR.ne', abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR.le _))]

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