OAI/Probability/SLEGauge/StochasticCalculus.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. instance OAI.ExactSLEGenerator.(instance at line 20) line 20
  2. instance OAI.ExactSLEGenerator.(instance at line 21) line 21
  3. abbrev OAI.ExactSLEGenerator.Driver line 22
  4. instance OAI.ExactSLEGenerator.(instance at line 23) line 23
  5. instance OAI.ExactSLEGenerator.(instance at line 24) line 24
  6. lemma OAI.ExactSLEGenerator.driver_eval_measurable line 25
  7. def OAI.ExactSLEGenerator.rawFiltration line 27
  8. def OAI.ExactSLEGenerator.increment line 30
  9. lemma OAI.ExactSLEGenerator.increment_measurable line 31
  10. lemma OAI.ExactSLEGenerator.increment_law line 33
  11. lemma OAI.ExactSLEGenerator.increment_integrable line 37
  12. lemma OAI.ExactSLEGenerator.increment_mean line 41
  13. lemma OAI.ExactSLEGenerator.increment_abs_moment_integrable line 45
  14. lemma OAI.ExactSLEGenerator.increment_sq_integrable line 50
  15. lemma OAI.ExactSLEGenerator.increment_second_moment line 54
  16. def OAI.ExactSLEGenerator.absMoment line 67
  17. lemma OAI.ExactSLEGenerator.absMoment_nonneg line 68
  18. lemma OAI.ExactSLEGenerator.gaussian_abs_moment line 70
  19. lemma OAI.ExactSLEGenerator.increment_abs_moment line 89
  20. lemma OAI.ExactSLEGenerator.increment_indep line 97
  21. lemma OAI.ExactSLEGenerator.increment_weighted_mean line 111
  22. lemma OAI.ExactSLEGenerator.increment_weighted_second_moment line 119
  23. theorem OAI.ExactSLEGenerator.expected_taylor_step line 132
  24. theorem OAI.ExactSLEGenerator.expected_taylor_sum line 190
  25. lemma OAI.ExactSLEGenerator.taylor_error_tendsto_zero line 231
  26. lemma OAI.ExactSLEGenerator.scalar_taylor_cubic line 247
  27. lemma OAI.ExactSLEGenerator.first_order_remainder line 287
  28. lemma OAI.ExactSLEGenerator.mixed_taylor_remainder line 319
  29. lemma OAI.ExactSLEGenerator.riemann_sum_error_le line 374