English
Let f: α → ℝ≥0 be a measurable density and g: α → E a Bochner integrable vector-valued function. If μ is a measure on α, then the vector measure obtained by multiplying g pointwise by f has the same total effect as first restricting μ by f and then applying the vector-density construction to g; i.e. μ.withDensityᵥ (f · g) = (μ.withDensity (λ x, f x)).withDensityᵥ g, under appropriate measurability and integrability hypotheses.
Русский
Пусть f: α → ℝ≥0 измерима функция плотности и g: α → E — векторно интегрируемая по Бочнеру функция. Тогда векторная мера, полученная умножением g на f точечно, эквивалентна сначала ограничению μ на плотность f и далее применению конструкции векторной плотности к g; то есть μ.withDensityᵥ (f · g) = (μ.withDensity (λ x, f x)).withDensityᵥ g при подходящих предпосылках измеримости и интегрируемости.
LaTeX
$$$\mu.withDensityᵥ (f \cdot g) = (\mu.withDensity (\lambda x. f x)).withDensityᵥ g$$$
Lean4
theorem withDensityᵥ_smul_eq_withDensityᵥ_withDensity {f : α → ℝ≥0} {g : α → E} (hf : AEMeasurable f μ)
(hfg : Integrable (f • g) μ) : μ.withDensityᵥ (f • g) = (μ.withDensity (fun x ↦ f x)).withDensityᵥ g :=
by
ext s hs
rw [withDensityᵥ_apply hfg hs, withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,
setIntegral_withDensity_eq_setIntegral_smul₀ hf.restrict _ hs]
simp only [Pi.smul_apply']
