1.17. ForMathlib.Probability.HasCondDistrib
A predicate for having a specified conditional distribution
Module LeanMachineLearning.ForMathlib.Probability.HasCondDistrib contains 26 exposed declarations.
-
ProbabilityTheory.hasCondDistrib_fst_prod -
ProbabilityTheory.HasCondDistrib.prod_right -
ProbabilityTheory.hasCondDistrib_prod_right_iff -
ProbabilityTheory.HasCondDistrib.indepFun_of_const -
ProbabilityTheory.IndepFun.hasCondDistrib_const -
ProbabilityTheory.hasCondDistrib_self -
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.of_measurableEmbedding_comp_right -
ProbabilityTheory.hasCondDistrib_measurableEmbedding_comp_right_iff -
ProbabilityTheory.hasCondDistrib_measurableEquiv_comp_right_iff -
ProbabilityTheory.hasCondDistrib_prodMk_left_unique_iff -
ProbabilityTheory.hasCondDistrib_prodMk_right_unique_iff -
MeasureTheory.Measure.dirac_compProd -
ProbabilityTheory.hasCondDistrib_const_iff -
ProbabilityTheory.HasCondDistrib.hasLaw_of_const' -
ProbabilityTheory.HasLaw.hasCondDistrib_const -
ProbabilityTheory.HasCondDistrib.measure_inter_preimage_eq_mul_of_eqOn_const -
ProbabilityTheory.HasCondDistrib.hasLaw_cond -
ProbabilityTheory.HasCondDistrib.indepFun_cond -
ProbabilityTheory.HasCondDistrib.condDistrib_eq -
ProbabilityTheory.hasCondDistrib_of_condDistrib_eq -
ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR