English
Let f: α → ℝ≥0∞ and g: α → E with appropriate measurability so that f.toReal · g is integrable. Then the vector measure μ.withDensityᵥ ((f) .toReal · g) equals the vector measure μ.withDensity f applied via g, i.e. μ.withDensityᵥ ((f x).toReal · g x) = (μ.withDensity f).withDensityᵥ g.
Русский
Пусть f: α → ℝ≥0∞ и g: α → E с подходящей измеримости, чтобы (f x).toReal · gx было интегрируемо. Тогда векторная мера μ.withDensityᵥ ((f) .toReal · g) равна μ.withDensity f применяемой к g, то есть μ.withDensityᵥ ((f x).toReal · g x) = (μ.withDensity f).withDensityᵥ g.
LaTeX
$$$\mu.withDensityᵥ \big((f)\!:\! α \to \mathbb{R}_{\ge 0}^{\infty} \ - toReal \cdot g\big) = (\mu.withDensity f).withDensityᵥ g$$$
Lean4
theorem withDensityᵥ_smul_eq_withDensityᵥ_withDensity' {f : α → ℝ≥0∞} {g : α → E} (hf : AEMeasurable f μ)
(hflt : ∀ᵐ x ∂μ, f x < ∞) (hfg : Integrable (fun x ↦ (f x).toReal • g x) μ) :
μ.withDensityᵥ (fun x ↦ (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g :=
by
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt), ←
withDensityᵥ_smul_eq_withDensityᵥ_withDensity hf.ennreal_toNNReal hfg]
apply congr_arg
ext
simp [NNReal.smul_def, ENNReal.coe_toNNReal_eq_toReal]
