OAI/Probability/SLEGauge/BrownianMartingales.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGenerator.compact_smooth_brownian_martingale line 21
  2. def OAI.ExactSLEOptional.roundUp line 54
  3. theorem OAI.ExactSLEOptional.le_roundUp line 56
  4. theorem OAI.ExactSLEOptional.roundUp_lt line 60
  5. theorem OAI.ExactSLEOptional.roundUp_le_iff line 67
  6. theorem OAI.ExactSLEOptional.roundUp_stopping line 73
  7. lemma OAI.ExactSLEOptional.roundUp_tendsto line 88
  8. lemma OAI.ExactSLEOptional.roundUp_le_add_one line 97
  9. lemma OAI.ExactSLEOptional.roundUp_countable_range line 103
  10. lemma OAI.ExactSLEOptional.stopped_measurable line 113
  11. lemma OAI.ExactSLEOptional.setIntegral_stopped_eq_terminal line 121
  12. lemma OAI.ExactSLEOptional.setIntegral_optional_sampling line 156
  13. def OAI.ExactSLEGenerator.generator line 175
  14. lemma OAI.ExactSLEGenerator.generator_continuous line 179
  15. lemma OAI.ExactSLEGenerator.compact_generator_bounds line 185
  16. theorem OAI.ExactSLEGenerator.compact_test_optional_sampling line 208
  17. abbrev OAI.ExactSLEMain.Driver line 260
  18. instance OAI.ExactSLEMain.(instance at line 261) line 261
  19. def OAI.ExactSLEMain.odeUntil line 263
  20. def OAI.ExactSLEMain.alive line 268
  21. def OAI.ExactSLEMain.loewnerMap line 271
  22. theorem OAI.ExactSLEMain.odeUntil_continuousOn line 275
  23. theorem OAI.ExactSLEMain.odeUntil_height_lower line 279
  24. theorem OAI.ExactSLEMain.loewner_vector_difference line 287
  25. theorem OAI.ExactSLEMain.odeUntil_unique line 316
  26. theorem OAI.ExactSLEMain.odeUntil_mono line 339
  27. theorem OAI.ExactSLEMain.alive_mono line 346
  28. theorem OAI.ExactSLEMain.loewnerMap_eq line 351
  29. def OAI.ExactSLEMain.shiftDriver line 357
  30. theorem OAI.ExactSLEMain.odeUntil_shift line 359
  31. theorem OAI.ExactSLEMain.loewnerMap_restart line 378