Structures · Analysis
ProbabilityTheory.IsMarkovKernel
A kernel is a Markov kernel if every measure in its image is a probability measure.
- Defined in
- Mathlib.Probability.Kernel.Defs
- Shape
- One type argument · adds isProbabilityMeasure
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every ProbabilityTheory.IsMarkovKernel is also a
Provided automatically by
Concrete types that are instances3
- Bool
- SFinKer.carrier
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by121
- ProbabilityTheory.Kernel.traj
- ProbabilityTheory.Kernel.traj_map_frestrictLe
- ProbabilityTheory.Kernel.trajContent
- ProbabilityTheory.Kernel.traj_comp_partialTraj
- ProbabilityTheory.Kernel.trajFun
- ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj
- ProbabilityTheory.Kernel.fst_compProd
- ProbabilityTheory.Kernel.bound_eq_one
- ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂
- ProbabilityTheory.Kernel.isSigmaSubadditive_trajContent
- ProbabilityTheory.Kernel.traj_map_updateFinset
- ProbabilityTheory.bayesRisk_le_avgRisk
- InformationTheory.integrable_llr_compProd_iff
- MeasureTheory.Measure.fst_compProd
- ProbabilityTheory.Kernel.integral_traj_partialTraj'
- ProbabilityTheory.Kernel.trajMeasure
- ProbabilityTheory.Kernel.eq_traj'
- ProbabilityTheory.Kernel.fst_prod
- DependsOn.lmarginalPartialTraj_of_le
- ProbabilityTheory.Kernel.partialTraj_compProd_traj
- ProbabilityTheory.Kernel.isProjectiveLimit_trajFun
- InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add
- ProbabilityTheory.bayesRisk_le_bayesRisk_comp
- ProbabilityTheory.Kernel.trajContent_cylinder
- ProbabilityTheory.Kernel.iIndepFun.of_subsingleton
- ProbabilityTheory.Kernel.IsMarkovKernel.map
- ProbabilityTheory.Kernel.compProd_apply_univ
- ProbabilityTheory.Kernel.partialTraj_comp_partialTraj'
- MeasureTheory.Measure.comp_apply_univ
- ProbabilityTheory.Kernel.snd_prod
- ProbabilityTheory.Kernel.trajContent_tendsto_zero
- ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂
- ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj
- ProbabilityTheory.Kernel.le_lmarginalPartialTraj_succ
- ProbabilityTheory.Kernel.trajContent_ne_top
- MeasureTheory.Measure.compProd_apply_univ
- ProbabilityTheory.Kernel.traj_eq_prod
- ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval
- ProbabilityTheory.lintegral_iInf_posterior_le_avgRisk
- ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply
- ProbabilityTheory.Kernel.setIntegral_traj_partialTraj
- ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj
- ProbabilityTheory.Kernel.iIndep.of_subsingleton
- ProbabilityTheory.Kernel.eq_traj
- InformationTheory.integrable_llr_of_integrable_llr_compProd
- ProbabilityTheory.Kernel.condExp_traj
- ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure
- ProbabilityTheory.Kernel.traj_apply
- ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd
- ConvexOn.apply_rnDeriv_ae_le_integral