Stoch

📁 Source: Mathlib/Probability/Kernel/Category/Stoch.lean

Statistics

Metric	Count
Definitions Stoch, StochHom, instMarkovCategoryStoch	3
Theorems instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory, instIsStableUnderBraidingSFinKerStochHom, instIsStableUnderComonoidSFinKerStochHom	3
Total	6

(root)

Definitions

Name	Category	Theorems
Stoch 📖	CompOp	—
StochHom 📖	CompOp	3 math math: instIsStableUnderComonoidSFinKerStochHom, instIsStableUnderBraidingSFinKerStochHom, instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory
instMarkovCategoryStoch 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel SFinKer.carrier CategoryTheory.WideSubcategory.obj SFinKer SFinKer.instLargeCategory StochHom SFinKer.str SFinKer.Hom.hom CategoryTheory.InducedWideCategory.Hom.hom CategoryTheory.WideSubcategory	—	CategoryTheory.InducedWideCategory.Hom.property
instIsStableUnderBraidingSFinKerStochHom 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBraiding SFinKer SFinKer.instLargeCategory instMonoidalCategorySFinKer CategoryTheory.SymmetricCategory.toBraidedCategory instSymmetricCategorySFinKer StochHom	—	ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.IsMarkovKernel.comp ProbabilityTheory.Kernel.instIsMarkovKernelProdParallelComp ProbabilityTheory.Kernel.IsMarkovKernel.map Measurable.prodMk Measurable.fst measurable_id' Measurable.snd measurable_const ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap
instIsStableUnderComonoidSFinKerStochHom 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComonoid SFinKer SFinKer.instLargeCategory instMonoidalCategorySFinKer StochHom instComonObjSFinKer	—	ProbabilityTheory.Kernel.instIsMarkovKernelPUnitDiscard ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy

---

← Back to Index