addHaar_preimage_smul — Mathlib

English

The image of a set under a homothety (translation plus scaling about a point) scales by |r^dim|

Русский

Образ множества при аффинном преобразовании типа гомотетии масштабируется на |r^dim|.

LaTeX

$$μ(A) = μ(homothety) μ(S) = |r^finrank| μ(S)$$

Lean4

@[simp]
theorem addHaar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : Set E) :
    μ ((r • ·) ⁻¹' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s :=
  calc
    μ ((r • ·) ⁻¹' s) = Measure.map (r • ·) μ s :=
      ((Homeomorph.smul (isUnit_iff_ne_zero.2 hr).unit).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s := by
      rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]

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