1.8. ForMathlib.Probability.Independence.CondDistrib🔗

Lemmas about conditional distributions

Module LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib contains 37 exposed declarations.

• ProbabilityTheory.map_swap_compProd_map_condDistribLemma · 0 deps
• ProbabilityTheory.condDistrib_prod_leftLemma · 0 deps
• ProbabilityTheory.condDistrib_condDistrib_ae_eq_sectR_condDistribLemma · 0 deps
• ProbabilityTheory.condDistrib_prod_self_leftLemma · 0 deps
• ProbabilityTheory.CondIndepFun.prod_rightLemma · 0 deps
• ProbabilityTheory.fst_condDistrib_prodLemma · 0 deps
• ProbabilityTheory.condDistrib_of_indepFunLemma · 0 deps
• ProbabilityTheory.indepFun_iff_condDistrib_eq_constLemma · 0 deps
• ProbabilityTheory.Measure.snd_compProd_prodMkLeftLemma · 0 deps
• ProbabilityTheory.Measure.snd_compProd_prodMkRightLemma · 0 deps
• ProbabilityTheory.Measure.snd_prodAssoc_compProd_prodMkLeftLemma · 0 deps
• ProbabilityTheory.Measure.map_swap_comprod_eq_fst_compProdLemma · 0 deps
• ProbabilityTheory.ProbabilityMeasure.ext_iff_coeLemma · 0 deps
• ProbabilityTheory.FiniteMeasure.ext_iff_coeLemma · 0 deps
• ProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearningInstance · 0 deps
• ProbabilityTheory.FiniteMeasure.le_iff_coeLemma · 1 deps
• ProbabilityTheory.instSubFiniteMeasure_leanMachineLearningInstance · 0 deps
• ProbabilityTheory.FiniteMeasure.sub_defLemma · 1 deps
• ProbabilityTheory.FiniteMeasure.toMeasure_subLemma · 1 deps
• ProbabilityTheory.instCanonicallyOrderedAddFiniteMeasure_leanMachineLearningInstance · 4 deps
• ProbabilityTheory.instOrderedSubFiniteMeasure_leanMachineLearningInstance · 3 deps
• ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iffLemma · 0 deps
• ProbabilityTheory.Kernel.prodMkRight_ae_eq_iffLemma · 0 deps
• ProbabilityTheory.condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRightLemma · 0 deps
• ProbabilityTheory.condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeftLemma · 0 deps
• ProbabilityTheory.«term𝓛[_|_;_]»Definition · 0 deps
• ProbabilityTheory.condIndepFun_fst_prodLemma · 0 deps
• ProbabilityTheory.indepFun_fst_prodLemma · 0 deps
• ProbabilityTheory.indepFun_snd_prodLemma · 0 deps
• ProbabilityTheory.measurableSet_graph'Lemma · 0 deps
• ProbabilityTheory.ae_eq_of_map_prodMk_eqLemma · 0 deps
• ProbabilityTheory.ae_eq_of_condDistrib_eq_deterministicLemma · 0 deps
• ProbabilityTheory.condDistrib_ae_eq_condLemma · 0 deps
• ProbabilityTheory.lintegral_condLemma · 0 deps
• ProbabilityTheory.condDistrib_prod_of_forall_condDistrib_condLemma · 0 deps
• ProbabilityTheory.cond_of_indepFunLemma · 0 deps
• ProbabilityTheory.cond_of_condIndepFunLemma · 0 deps