English
For f: X → 𝕜 and c ∈ E, ∫ f(x) • c dμ = (∫ f(x) dμ) • c.
Русский
Пусть f: X → 𝕜 и c ∈ E; тогда интеграл от f(x) • c равен интегралу f(x) умноженному на c.
LaTeX
$$$\\int_X f(x) \\cdot c \\,d\\mu = \\left(\\int_X f(x) \\,d\\mu\\right) \\cdot c$$$
Lean4
theorem integral_smul_const {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [CompleteSpace E] (f : X → 𝕜) (c : E) :
∫ x, f x • c ∂μ = (∫ x, f x ∂μ) • c := by
by_cases hf : Integrable f μ
· exact ((1 : 𝕜 →L[𝕜] 𝕜).smulRight c).integral_comp_comm hf
· by_cases hc : c = 0
· simp [hc, integral_zero, smul_zero]
rw [integral_undef hf, integral_undef, zero_smul]
rw [integrable_smul_const hc]
simp_rw [hf, not_false_eq_true]
/-
Note that the integrability hypothesis in the two lemmas below is necessary: consider the case
where `A = ℝ × ℝ`, `c = (1,0)`, and `f` is only integrable on the first component.
-/
