integral_continuousLinearMap_prod

English

For sets s,t, and integrable f on s×t, the integral over (μ×ν) restricted to s×t equals the iterated integral over s and t separately.

Русский

Для множеств s,t и интегрируемой функции f на s×t интеграл по (μ×ν) ограниченному на s×t равен итерационному интегралу по s и t по отдельности.

LaTeX

$$$$\\int z \\in s × t, f(z) \\, d(μ×ν) = \\int x \\in s, \\int y \\in t, f(x,y) \\, dν \\, dμ.$$$$

Lean4

theorem integral_continuousLinearMap_prod (hμ : Integrable id μ) (hν : Integrable id ν) :
    ∫ p, L p ∂(μ.prod ν) = ∫ x, L.comp (.inl ℝ E F) x ∂μ + ∫ y, L.comp (.inr ℝ E F) y ∂ν :=
  integral_continuousLinearMap_prod' (ContinuousLinearMap.integrable_comp _ hμ)
    (ContinuousLinearMap.integrable_comp _ hν)

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