OAI/Probability/SpanningForest/BrownianCanonicalPosterior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.Observation.gaussianFiniteTilt_finset_eq line 13
2. theorem OAI.Problem336.Observation.finiteTiltMean_eq_condExp_brownian_history line 31
3. theorem OAI.Problem336.Observation.drift_eq_condExp_brownian_history line 86
4. theorem OAI.Problem336.Observation.drift_zero_zero line 112
5. theorem OAI.Problem336.Observation.drift_eq_condExp_brownian_history_zero line 119
6. theorem OAI.Problem336.Observation.drift_eq_condExp_brownian_history_all_times line 167