eval_integral — Mathlib

English

If f: X → Π_i E_i is integrable coordinatewise, then the integral of f equals the vector of integrals of each coordinate: ∫ f dμ = (∫ f_i dμ)_i.

Русский

Пусть f: X → Π_i E_i интегрируема по координатам; интеграл функции равен вектору координатных интегралов: ∫ f dμ = (∫ f_i dμ)_i.

LaTeX

$$$$\\forall i,\\; \\int x\, f(x)\\,d\\mu = \\Bigl(\\int x\, f(x)_i\,d\\mu\\Bigr)_i.$$$$

Lean4

theorem eval_integral (hf : ∀ i, Integrable (f · i) μ) (i : ι) : (∫ x, f x ∂μ) i = ∫ x, f x i ∂μ := by
  simp [← ContinuousLinearMap.proj_apply (R := ℝ) i (∫ x, f x ∂μ),
    ← ContinuousLinearMap.integral_comp_comm _ (Integrable.of_eval hf)]

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