OAI/Probability/SKValue/Equations/BrownianIncrementIndepPast.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.brownian_increment_indep_past line 26
  2. lemma OAI.SKValue.brownian_increment_integral line 42
  3. lemma OAI.SKValue.brownian_increment_second_moment line 49
  4. lemma OAI.SKValue.brownian_predictable_increment_integrable line 62
  5. lemma OAI.SKValue.brownian_predictable_increment_mean line 71
  6. lemma OAI.SKValue.brownian_predictable_quadratic_integrable line 82
  7. lemma OAI.SKValue.brownian_predictable_quadratic_mean line 96
  8. def OAI.SKValue.driftDefect line 122
  9. lemma OAI.SKValue.driftDefect_nonneg line 128
  10. lemma OAI.SKValue.driftDefect_error_bound line 132
  11. lemma OAI.SKValue.driftDefect_tendsto line 194