Theorems · Theorem · probability

ProbabilityTheory.condExpKernel_def

∀ {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω),
  ProbabilityTheory.condExpKernel μ m =
    if _h : Nonempty Ω then (ProbabilityTheory.condDistrib id id μ).comap id ⋯ else 0

Defined in: Mathlib.Probability.Kernel.Condexp
Cited by: 1 results in Mathlib
Foundations: Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace StandardBorelSpace MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ProbabilityTheory.Kernelstatement · cited by 1,281
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
StandardBorelSpacestatement and proof · cited by 304
ProbabilityTheory.condDistribstatement and proof · cited by 58
ProbabilityTheory.condExpKernelstatement · cited by 49
ProbabilityTheory.Kernel.comapstatement and proof · cited by 34

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.condExpKernel_eqproof · cited by 8