Integrals split by finite measurable partitions #
A measurable finite partition of a measure space decomposes integrals on the product space into finite sums over partition rectangles.
theorem
Finpartition.setIntegral_prod_eq_sum_parts
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(R : Finpartition Set.univ)
(hR : ∀ r ∈ R.parts, MeasurableSet r)
{S T : Set Ω}
(hS : MeasurableSet S)
(hT : MeasurableSet T)
{f : Ω × Ω → ℝ}
(hf : MeasureTheory.IntegrableOn f (S ×ˢ T) (μ.prod μ))
:
A finite measurable partition of the carrier cuts a rectangle into finitely many disjoint subrectangles, splitting any integral over it into a finite sum.
theorem
Finpartition.integral_eq_sum_parts
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(R : Finpartition Set.univ)
(hR : ∀ r ∈ R.parts, MeasurableSet r)
{f : Ω × Ω → ℝ}
(hf : MeasureTheory.Integrable f (μ.prod μ))
:
A finite measurable partition of the carrier splits an integral over the whole product carrier into a finite sum over its rectangles.