OAI/Probability/SpanningForest/CountableBrownian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.CountableBrownian.pullbackTimes line 14
2. lemma OAI.Problem336.CountableBrownian.measurable_pullbackTimes line 19
3. def OAI.Problem336.CountableBrownian.family line 23
4. instance OAI.Problem336.CountableBrownian.family_probability line 26
5. instance OAI.Problem336.CountableBrownian.family_isGaussian line 31
6. lemma OAI.Problem336.CountableBrownian.family_projective line 40
7. theorem OAI.Problem336.CountableBrownian.exists_countable_brownian_law line 52
8. theorem OAI.Problem336.CountableBrownian.hasLaw_increment line 57
9. theorem OAI.Problem336.CountableBrownian.hasLaw_eval line 77
10. theorem OAI.Problem336.CountableBrownian.isGaussianProcess line 95
11. lemma OAI.Problem336.CountableBrownian.integral_eval line 102
12. lemma OAI.Problem336.CountableBrownian.covariance_eval line 107