OAI/Probability/SpanningForest/BrownianBridge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.BrownianBridge.residual line 15
  2. theorem OAI.Problem336.BrownianBridge.indepFun_residual_endpoint line 18
  3. theorem OAI.Problem336.BrownianBridge.indepFun_regroup line 52
  4. theorem OAI.Problem336.BrownianBridge.residual_add_linear line 85
  5. theorem OAI.Problem336.BrownianBridge.indepFun_residual_hidden_endpoint line 92
  6. theorem OAI.Problem336.BrownianBridge.history_comap_eq_endpoint_residual line 113
  7. theorem OAI.Problem336.BrownianBridge.isGaussianProcess_independent_family line 136
  8. theorem OAI.Problem336.BrownianBridge.observation_history_comap line 159
  9. theorem OAI.Problem336.BrownianBridge.indepFun_residual_family_endpoint line 168
  10. theorem OAI.Problem336.BrownianBridge.indepFun_residual_family_hidden_endpoint line 209
  11. theorem OAI.Problem336.BrownianBridge.observation_family_history_comap line 238