1.18. ForMathlib.Probability.Kernel.IonescuTulcea.Traj🔗

Lemmas about traj and trajMeasure

Module LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj contains 12 exposed declarations.

• coe_default_Iic_zeroLemma · 0 deps
• ProbabilityTheory.Kernel.traj_zero_map_eval_zeroLemma · 0 deps
• MeasurableEquiv.IicSuccProdDefinition · 0 deps
• ProbabilityTheory.Kernel.symm_IicSuccProdLemma · 1 deps
• ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_applyLemma · 1 deps
• ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongrLemma · 0 deps
• ProbabilityTheory.Kernel.MeasurableEquiv.coe_reflLemma · 0 deps
• ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib'Lemma · 0 deps
• ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistribLemma · 0 deps
• ProbabilityTheory.Kernel.trajMeasure_map_frestrictLeLemma · 0 deps
• ProbabilityTheory.Kernel.eq_trajMeasure_map_frestrictLeLemma · 0 deps
• ProbabilityTheory.Kernel.hasLaw_trajMeasureLemma · 0 deps