OAI/Probability/FreeIsing/Estimates/FiniteIsingInnovation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteIsingFiltering.innovation line 19
  2. theorem OAI.Problem367.FiniteIsingFiltering.innovation_stronglyAdapted line 23
  3. theorem OAI.Problem367.FiniteIsingFiltering.continuous_innovation line 33
  4. theorem OAI.Problem367.FiniteIsingFiltering.innovation_increment_drift_bound line 43
  5. theorem OAI.Problem367.FiniteIsingFiltering.innovation_martingale_of_posterior line 81
  6. theorem OAI.Problem367.FiniteIsingFiltering.innovation_isBrownianReal_of_posterior line 103
  7. theorem OAI.Problem367.FiniteIsingFiltering.innovation_unit_projection_condExp_character_of_posterior line 126
  8. theorem OAI.Problem367.FiniteIsingFiltering.innovation_increment_law_and_indep_of_posterior line 194
  9. theorem OAI.Problem367.FiniteIsingFiltering.innovation_increment_indep_filtration_of_posterior line 223
  10. theorem OAI.Problem367.FiniteIsingFiltering.innovation_future_indep_filtration_of_posterior line 234
  11. theorem OAI.Problem367.FiniteIsingFiltering.mean_eq_condExp line 264
  12. theorem OAI.Problem367.FiniteIsingFiltering.innovation_martingale line 275
  13. theorem OAI.Problem367.FiniteIsingFiltering.innovation_isBrownianReal line 282
  14. theorem OAI.Problem367.FiniteIsingFiltering.innovation_increment_law_and_indep line 288
  15. theorem OAI.Problem367.FiniteIsingFiltering.innovation_increment_indep_filtration line 303
  16. theorem OAI.Problem367.FiniteIsingFiltering.innovation_future_indep_filtration line 311