English
If μ is scaled by r, then (r • μ).withDensity f = r • μ.withDensity f.
Русский
Если мера μ умножить на r, то (r • μ).withDensity f = r • μ.withDensity f.
LaTeX
$$$\text{withDensity}(r\cdot μ, f) = r \cdot (μ.withDensity f)$$$
Lean4
theorem withDensity_smul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : Measurable f) : μ.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 hf]
simp only [Pi.smul_apply, smul_eq_mul]