Theorems · Theorem · probability

ProbabilityTheory.Kernel.prod_const

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure γ)
  [MeasureTheory.SFinite ν],
  (ProbabilityTheory.Kernel.const α μ).prod (ProbabilityTheory.Kernel.const α ν) =
    ProbabilityTheory.Kernel.const α (μ.prod ν)

Defined in

Mathlib.Probability.Kernel.Composition.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SFiniteMeasureTheory.SFinite