1.28. ForMathlib.Probability.Kernel.IonescuTulcea.Traj🔗

Lemmas about traj and trajMeasure

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

• ProbabilityTheory.Kernel.traj_zero_map_eval_zeroLemma · 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
• ProbabilityTheory.Kernel.iicOfFinDefinition · 1 deps
• ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicHAddOfNatIicOfFinInstance · 2 deps
• ProbabilityTheory.Kernel.trajMeasureFinDefinition · 2 deps
• ProbabilityTheory.Kernel.instIsProbabilityMeasureForallTrajMeasureFinInstance · 4 deps
• ProbabilityTheory.Kernel.trajMeasureFin_defLemma · 4 deps
• ProbabilityTheory.Kernel.hasLaw_eval_zero_trajMeasureLemma · 0 deps
• ProbabilityTheory.Kernel.hasLaw_eval_zero_trajMeasureFinLemma · 3 deps
• ProbabilityTheory.Kernel.hasCondDistrib_trajMeasureFinLemma · 3 deps
• ProbabilityTheory.Kernel.hasLaw_trajMeasureFinLemma · 3 deps
• ProbabilityTheory.Kernel.eq_trajMeasureFin_mapLemma · 3 deps