English
If c is a scalar and f is integrable, then ∫ c·f = c·∫ f.
Русский
Если скаляр c и функция f интегрируемы, то интеграл от c·f равен c· интеграл от f.
LaTeX
$$$\int a, c \cdot f(a) \partial\mu = c \cdot \int a, f(a) \partial\mu$$$
Lean4
/-- The Bochner integral is linear. Note this requires `𝕜` to be a normed division ring, in order
to ensure that for `c ≠ 0`, the function `c • f` is integrable iff `f` is. For an analogous
statement for more general rings with an *a priori* integrability assumption on `f`, see
`MeasureTheory.Integrable.integral_smul`. -/
@[integral_simps]
theorem integral_smul [Module 𝕜 G] [NormSMulClass 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G) :
∫ a, c • f a ∂μ = c • ∫ a, f a ∂μ := by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f
· simp [integral, hG]
