English
Let μ and ν be measures on X, and s a set with finite μ s and ν s (i.e., μ s ≠ ∞ and ν s ≠ ∞). Then the weighted smul for the sum of measures equals the sum of the weighted smuls: weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s.
Русский
Пусть μ и ν — меры на X, s — множество так, что μ(s) и ν(s) конечны. Тогда взвешенная умножение по сумме мер равно сумме взвешенных умножений: weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s.
LaTeX
$$$$weightedSMul(\mu + \nu)\, s = weightedSMul(\mu)\, s + weightedSMul(\nu)\, s.$$$$
Lean4
/-- Given a set `s`, return the continuous linear map `fun x => μ.real s • x`. The extension
of that set function through `setToL1` gives the Bochner integral of L1 functions. -/
def weightedSMul {_ : MeasurableSpace α} (μ : Measure α) (s : Set α) : F →L[ℝ] F :=
μ.real s • ContinuousLinearMap.id ℝ F
