English
There is a scalar action of a scalar type R on measures, defined by scaling the outer measure. The action makes the measure space into an R-module; in particular, (c • μ) is obtained by scaling the outer measure: (c • μ).toOuterMeasure = c • μ.toOuterMeasure.
Русский
Существует действие скаляра R на множества мер, задаваемое масштабированием внешней меры. Пространство мер образует модуль над R; в частности, (c • μ) получается умножением внешней меры на c: (c • μ).toOuterMeasure = c • μ.toOuterMeasure.
LaTeX
$$$\exists \cdot : R \times \text{Measure}(\alpha) \to \text{Measure}(\alpha),\; \forall c,\mu:\; (c \cdot \mu).toOuterMeasure = c \cdot \mu.toOuterMeasure \land \forall s:\; (c \cdot \mu)(s) = c \cdot \mu(s).$$$
Lean4
instance instSMul {_ : MeasurableSpace α} : SMul R (Measure α) :=
⟨fun c μ =>
{ toOuterMeasure := c • μ.toOuterMeasure
m_iUnion := fun s hs hd => by
simp only [OuterMeasure.smul_apply, coe_toOuterMeasure, ENNReal.tsum_const_smul, measure_iUnion hd hs]
trim_le := by rw [OuterMeasure.trim_smul, μ.trimmed] }⟩
