addHaar_smul_of_nonneg — Mathlib

English

Scaling a set by nonnegative factor r scales Haar measure by |r|^{finrank}.

Русский

Масштабирование множества на неотрицательный коэффициент r масштабирует гааровскую меру на |r|^{финрегистров}.

LaTeX

$$μ(r•S) = |r|^{finrank} μ(S)$$

Lean4

theorem addHaar_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) (s : Set E) : μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s :=
  by rw [addHaar_smul, abs_pow, abs_of_nonneg hr]

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