Theorems · Theorem · probability

ProbabilityTheory.condDistrib_def

∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {x : MeasurableSpace α} [inst_3 : MeasurableSpace β] (Y : α → Ω) (X : α → β)
  (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).condKernel

Defined in

Mathlib.Probability.Kernel.CondDistrib

Cited by

12 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpaceMeasureTheory.IsFiniteMeasure