integral_comp — Mathlib

English

Restricted product integral where the β-part is univ; equals iterated integral over t.

Русский

Ограниченный по β-интеграл, где β=univ; равен повторному интегралу по t.

LaTeX

$$$\int z in s × univ, f(z) d(κ ⊗ η)a = \int x in s, ∫ y f(x,y) dη(a,x) dκ a$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_comp [NormedSpace ℝ E] ⦃f : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) :
    Integrable (fun x ↦ ∫ y, f y ∂η x) (κ a) :=
  Integrable.mono hf.integral_norm_comp hf.1.integral_kernel_comp <|
    ae_of_all _ fun _ ↦
      (norm_integral_le_integral_norm _).trans_eq
        (norm_of_nonneg <| integral_nonneg_of_ae <| ae_of_all _ fun _ ↦ norm_nonneg _).symm

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