integral_norm_prod_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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