integral_norm_comp — Mathlib

English

Equality of the full product integral and the iterated integral for integrable f.

Русский

Согласование полной интеграции по произведению и итеративного интеграла для интегрируемой f.

LaTeX

$$$\int z f z \, d(κ ⊗ η)a = \int x \int y f(x,y) \, dη(a,x) \, dκ a$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_norm_comp ⦃f : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) :
    Integrable (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) :=
  ((integrable_comp_iff hf.1).1 hf).2

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