integral_const_mul_of_integrable — Mathlib

English

For a fixed c ∈ A and integrable f: X → A, ∫ c · f(x) dμ = c · ∫ f(x) dμ.

Русский

Для фиксированного c ∈ A и интегрируемой функции f: X → A выполняется ∫ c · f(x) dμ = c · ∫ f(x) dμ.

LaTeX

$$$\\int_X c \\cdot f(x) \\,d\\mu = c \\cdot \\left(\\int_X f(x) \\,d\\mu\\right)$$$

Lean4

theorem integral_const_mul_of_integrable {A : Type*} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A]
    [SMulCommClass ℝ A A] {f : X → A} (hf : Integrable f μ) {c : A} : ∫ x, c * f x ∂μ = c * ∫ x, f x ∂μ :=
  by
  by_cases hA : CompleteSpace A
  · change ∫ x, ContinuousLinearMap.mul ℝ _ c (f x) ∂μ = ContinuousLinearMap.mul ℝ _ c (∫ x, f x ∂μ)
    rw [ContinuousLinearMap.integral_comp_comm _ hf]
  · simp [integral, hA]

Похожие утверждения