setIntegral_compProd_univ_right — Mathlib

English

A primed variant stating that the integral of the sum equals the sum of integrals, when integrating over the product kernel.

Русский

Примечание: интеграл суммы равен сумме интегралов при интегрировании по произведённому ядру.

LaTeX

$$Eq(∫ κ a (f+g) = ∫ κ a (f) + ∫ κ a (g))$$

Lean4

theorem setIntegral_compProd_univ_right (f : β × γ → E) {s : Set β} (hs : MeasurableSet s)
    (hf : IntegrableOn f (s ×ˢ univ) ((κ ⊗ₖ η) a)) :
    ∫ z in s ×ˢ univ, f z ∂(κ ⊗ₖ η) a = ∫ x in s, ∫ y, f (x, y) ∂η (a, x) ∂κ a := by
  simp_rw [setIntegral_compProd hs MeasurableSet.univ hf, Measure.restrict_univ]

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