const_smul — Mathlib

English

If r ≥ 0, then the Haar measure of the preimage under scaling by r scales by |r^finrank|.

Русский

Если r ≥ 0, то мера по предобразу масштабирования на r масштабируется на |r^{finrank}|.

LaTeX

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

Lean4

theorem const_smul (hs : NullMeasurableSet s μ) (r : ℝ) : NullMeasurableSet (r • s) μ :=
  by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · simp
  obtain rfl | hr := eq_or_ne r 0
  · simpa [zero_smul_set hs'] using nullMeasurableSet_singleton _
  obtain ⟨t, ht, hst⟩ := hs
  refine ⟨_, ht.const_smul_of_ne_zero hr, ?_⟩
  rw [← measure_symmDiff_eq_zero_iff] at hst ⊢
  rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]

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