Theorems · Theorem · probability
ProbabilityTheory.condKernel_compProd
∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α Ω) [inst_4 : ProbabilityTheory.IsMarkovKernel κ], ⇑(μ.compProd κ).condKernel =ᵐ[μ] ⇑κ- Cited by
- 0 results in Mathlib
- Foundations
- Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.aestatement and proof · cited by 2,352
- Filter.EventuallyEqstatement and proof · cited by 1,912
- ProbabilityTheory.Kernelstatement and proof · cited by 1,281
- MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
- Filter.EventuallyEq.symmproof · cited by 408
- StandardBorelSpacestatement and proof · cited by 304
- MeasureTheory.Measure.compProdstatement and proof · cited by 132
- ProbabilityTheory.IsMarkovKernelstatement and proof · cited by 124
- MeasureTheory.Measure.fstproof · cited by 70
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.