OAI/Probability/SLEGauge/RadiusComparison.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.actual_radius_eq_full line 23
  2. lemma OAI.ExactSLEGreen.physicalClock_radius line 30
  3. lemma OAI.ExactSLEGreen.actual_clock_eq line 37
  4. lemma OAI.ExactSLEGreen.actual_speed_eq line 53
  5. lemma OAI.ExactSLEMain.exp_clock_integral line 61
  6. lemma OAI.ExactSLEMain.activeODEClock_monotone line 82
  7. theorem OAI.ExactSLEGreen.actual_regularized_pair_discount line 91
  8. lemma OAI.ExactSLEGreen.actual_regularized_single_discount line 179
  9. def OAI.ExactSLEGreen.unfinishedCutoffTop line 224
  10. def OAI.ExactSLEGreen.unfinishedCutoff line 231
  11. def OAI.ExactSLEStops.insert line 242
  12. def OAI.ExactSLEStops.sort line 245
  13. lemma OAI.ExactSLEStops.insert_length line 249
  14. lemma OAI.ExactSLEStops.sort_length line 255
  15. lemma OAI.ExactSLEStops.insert_stopping line 259
  16. lemma OAI.ExactSLEStops.sort_stopping line 274
  17. lemma OAI.ExactSLEStops.insert_perm line 283
  18. lemma OAI.ExactSLEStops.sort_perm line 294
  19. lemma OAI.ExactSLEStops.insert_sorted line 300
  20. lemma OAI.ExactSLEStops.sort_sorted line 316
  21. lemma OAI.ExactSLEStops.no_change_between line 323
  22. lemma OAI.ExactSLEStops.deferred_stopping line 351
  23. lemma OAI.ExactSLEStops.finset_inf_stopping line 362
  24. lemma OAI.ExactSLEStops.sort_bounded line 379
  25. lemma OAI.ExactSLEGreen.unfinishedCutoffTop_le line 391
  26. lemma OAI.ExactSLEGreen.unfinishedCutoff_coe line 395
  27. lemma OAI.ExactSLEGreen.unfinishedCutoff_stopping line 401
  28. lemma OAI.ExactSLEGreen.unfinishedCutoff_before_individual line 431