intervalIntegral_comp_comm — Mathlib

English

Let L be a continuous linear map E →L[𝕜] F and let f be an interval-integrable function with values in E. Then the integral of L applied to f equals L applied to the integral of f; i.e., ∫_a^b L(f(x)) dμ = L(∫_a^b f(x) dμ).

Русский

Пусть L: E →L[𝕜] F — непрерывное линейное отображение, а f: ℝ → E удовлетворяет условию интервального интегрирования на [a, b]. Тогда интеграл L(f(x)) по x равен L интегралу f(x) по x: ∫_a^b L(f(x)) dμ = L(∫_a^b f(x) dμ).

LaTeX

$$$$\int_{a}^{b} L(f(x)) \, d\mu = L\left( \int_{a}^{b} f(x) \, d\mu \right).$$$$

Lean4

theorem _root_.ContinuousLinearMap.intervalIntegral_comp_comm [CompleteSpace E] (L : E →L[𝕜] F)
    (hf : IntervalIntegrable f μ a b) : (∫ x in a..b, L (f x) ∂μ) = L (∫ x in a..b, f x ∂μ) := by
  simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]

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