integral_prod_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem integral_prod_left ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) : Integrable (fun x => ∫ y, f (x, y) ∂ν) μ :=
  Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right' <|
    Eventually.of_forall fun x =>
      (norm_integral_le_integral_norm _).trans_eq <|
        (norm_of_nonneg <| integral_nonneg_of_ae <| Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm

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