withDensity_smul — Mathlib

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]

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