OAI/Probability/SpanningForest/InnovationMartingale.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.Innovation.integrable_bounded_field line 12
  2. theorem OAI.Problem336.Innovation.integral_integrated_drift line 24
  3. theorem OAI.Problem336.Innovation.integral_posterior_on_past line 38
  4. theorem OAI.Problem336.Innovation.integral_integrated_posterior line 50
  5. theorem OAI.Problem336.Innovation.integrable_integrated_field line 64
  6. theorem OAI.Problem336.Innovation.intervalIntegrable_field line 76
  7. def OAI.Problem336.Innovation.innovation line 88
  8. theorem OAI.Problem336.Innovation.innovation_sub line 92
  9. theorem OAI.Problem336.Innovation.integrable_innovation line 105
  10. theorem OAI.Problem336.Innovation.integral_innovation_sub line 113
  11. theorem OAI.Problem336.Innovation.martingale_innovation line 137
  12. theorem OAI.Problem336.Innovation.condExp_innovation_sub_eq_zero line 161
  13. theorem OAI.Problem336.Innovation.integral_weighted_eq_zero_of_condExp line 174
  14. theorem OAI.Problem336.Innovation.integral_weighted_innovation_sub_eq_zero line 194
  15. def OAI.Problem336.Innovation.nnInnovation line 210
  16. theorem OAI.Problem336.Innovation.nnInnovation_apply line 215
  17. theorem OAI.Problem336.Innovation.integral_integrated_posterior_nnreal line 220
  18. theorem OAI.Problem336.Innovation.martingale_nnInnovation line 240
  19. theorem OAI.Problem336.Innovation.integral_weighted_martingale_sub_eq_zero line 286
  20. theorem OAI.Problem336.Innovation.innovation_sub_noise_bound line 302