English
For a field 𝕜 with nontrivial norm, and f: α → E, the withDensityᵥ construction commutes with scalar multiplication: μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f.
Русский
Для поля 𝕜 с ненулевой нормой и функции f: α → E верно: μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f.
LaTeX
$$$ μ.withDensityᵥ (r \\cdot f) = r \\cdot μ.withDensityᵥ f $$$
Lean4
@[simp]
theorem withDensityᵥ_smul {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] (f : α → E)
(r : 𝕜) : μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f :=
by
by_cases hf : Integrable f μ
· ext1 i hi
rw [withDensityᵥ_apply (hf.smul r) hi, VectorMeasure.smul_apply, withDensityᵥ_apply hf hi, ← integral_smul r f]
simp only [Pi.smul_apply]
· by_cases hr : r = 0
· rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
· rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, smul_zero]
rwa [integrable_smul_iff hr f]
