English
For a scalar r and a vector measure v, the scaled vector measure r · v is defined by (r · v)(S) = r · v(S) for all sets S.
Русский
Для скаляра r и векторной меры v определена масштабированная мера (r · v)(S) = r · v(S) для всех множеств S.
LaTeX
$$def smul (r : R) (v : VectorMeasure α M) : VectorMeasure α M$$
Lean4
/-- Given a scalar `r` and a vector measure `v`, `smul r v` is the vector measure corresponding to
the set function `s : Set α => r • (v s)`. -/
def smul (r : R) (v : VectorMeasure α M) : VectorMeasure α M
where
measureOf' := r • ⇑v
empty' := by rw [Pi.smul_apply, empty, smul_zero]
not_measurable' _ hi := by rw [Pi.smul_apply, v.not_measurable hi, smul_zero]
m_iUnion' _ hf₁ hf₂ := by exact HasSum.const_smul _ (v.m_iUnion hf₁ hf₂)
