Theorems · Theorem · probability

MeasureTheory.Measure.compProd_sum_left

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {ι : Type u_3} [Countable ι] {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), MeasureTheory.SFinite (μ i)],
  (MeasureTheory.Measure.sum μ).compProd κ = MeasureTheory.Measure.sum fun i => (μ i).compProd κ

Defined in

Mathlib.Probability.Kernel.Composition.MeasureCompProd

Cited by

0 results in Mathlib

Foundations

Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableMeasureTheory.SFinite