OAI/Probability/SpanningForest/InnovationIdentification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.InnovationIdentification.restrict_map_eq_smul_of_characteristic line 16
2. theorem OAI.Problem336.InnovationIdentification.law_and_indep_of_past_characteristic line 31
3. theorem OAI.Problem336.InnovationIdentification.iIndepFun_of_past_characteristic line 56
4. theorem OAI.Problem336.InnovationIdentification.hasLaw_infinitePi_of_past_characteristic line 92
5. theorem OAI.Problem336.InnovationIdentification.hasIndepIncrements_of_past_characteristic line 112
6. theorem OAI.Problem336.InnovationIdentification.isPreBrownianReal_of_past_characteristic line 137
7. theorem OAI.Problem336.InnovationIdentification.isBrownianReal_of_past_characteristic line 160
8. theorem OAI.Problem336.InnovationIdentification.hasIndepIncrements_of_strict_past_characteristic line 172
9. theorem OAI.Problem336.InnovationIdentification.isPreBrownianReal_of_strict_past_characteristic line 188