withDensity_smul' — Mathlib

English

If r ≠ ∞, then μ.withDensity (r • f) = r • μ.withDensity f.

Русский

Если r не бесконечно, то μ.withDensity (r • f) = r • μ.withDensity f.

LaTeX

$$$r \neq \infty \Rightarrow \mu.withDensity (r \cdot f) = r \cdot \mu.withDensity f$$$

Lean4

theorem withDensity_smul' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) : μ.withDensity (r • f) = r • μ.withDensity f :=
  by
  refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs, smul_eq_mul, ←
    lintegral_const_mul' r f hr]
  simp only [Pi.smul_apply, smul_eq_mul]

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