integral_mul_const_of_integrable — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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