integral_prod_right — Mathlib

English

If f is integrable on μ×ν, then the function y ↦ ∫ x f(x,y) dμ is integrable with respect to ν.

Русский

Если f интегрируема на μ×ν, то y ↦ ∫ f(x,y) dx интегрируема по ν.

LaTeX

$$$\mathrm{Integrable}(f, μ×ν) \Rightarrow \mathrm{Integrable}\left(y \mapsto \int x f(x,y) dμ\right) ν$$$

Lean4

theorem integral_prod_right [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
    Integrable (fun y => ∫ x, f (x, y) ∂μ) ν :=
  hf.swap.integral_prod_left

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