1.7. ForMathlib.Probability.HasCondDistrib
A predicate for having a specified conditional distribution
Module LeanMachineLearning.ForMathlib.Probability.HasCondDistrib contains 12 exposed declarations.
-
ProbabilityTheory.hasCondDistrib_fst_prod -
ProbabilityTheory.HasCondDistrib.prod_right -
ProbabilityTheory.hasCondDistrib_prod_right_iff -
ProbabilityTheory.HasCondDistrib.indepFun_of_const -
ProbabilityTheory.HasCondDistrib.const_map_of_const -
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib -
ProbabilityTheory.HasCondDistrib.hasLaw_comp -
ProbabilityTheory.HasCondDistrib.prod -
ProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic -
ProbabilityTheory.HasCondDistrib.condDistrib_eq -
ProbabilityTheory.hasCondDistrib_of_condDistrib_eq -
ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR