OAI/Probability/SLEGauge/CutoffExhaustion.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.unfinishedCutoff_exhausts line 26
  2. theorem OAI.ExactSLEGreen.actual_unfinished_cutoff line 60
  3. lemma OAI.ExactSLEGreen.localState_noiseFree_deriv line 78
  4. lemma OAI.ExactSLEGreen.localState_lower_cutoff line 91
  5. lemma OAI.ExactSLEGreen.localState_noise_bounds line 115
  6. lemma OAI.ExactSLEGreen.finite_pos_lower line 141
  7. theorem OAI.ExactSLEGreen.actual_common_cutoff_safe line 158
  8. def OAI.ExactSLEStops.clip line 227
  9. lemma OAI.ExactSLEStops.clip_coe line 230
  10. lemma OAI.ExactSLEStops.clip_le line 234
  11. lemma OAI.ExactSLEStops.le_clip_iff line 239
  12. lemma OAI.ExactSLEStops.clip_le_time line 243
  13. lemma OAI.ExactSLEStops.clip_stopping line 245
  14. def OAI.ExactSLEStops.phase line 256
  15. lemma OAI.ExactSLEStops.phase_measurable line 258
  16. lemma OAI.ExactSLEStops.phase_one_iff line 267
  17. lemma OAI.ExactSLEStops.phase_two_iff line 272
  18. lemma OAI.ExactSLEStops.phase_zero_iff line 276
  19. lemma OAI.ExactSLEStops.phase_three_iff line 280
  20. lemma OAI.ExactSLEStops.no_actual_change_between line 286
  21. lemma OAI.ExactSLEGreen.radialTime_antitone line 306
  22. lemma OAI.ExactSLEGreen.actual_radius_before_target line 314
  23. lemma OAI.ExactSLEGreen.actual_physicalClock_le line 330
  24. lemma OAI.ExactSLEGreen.actual_physicalClock_at line 344
  25. def OAI.ExactSLEGreen.levelRadius line 359
  26. def OAI.ExactSLEGreen.levelTime line 360
  27. lemma OAI.ExactSLEGreen.levelRadius_pos line 362
  28. lemma OAI.ExactSLEGreen.levelRadius_le line 364
  29. lemma OAI.ExactSLEGreen.levelRadius_antitone line 368
  30. lemma OAI.ExactSLEGreen.levelTime_mono line 373
  31. lemma OAI.ExactSLEGreen.levelRadius_clock line 380
  32. lemma OAI.ExactSLEGreen.levelTime_clock line 388
  33. lemma OAI.ExactSLEGreen.levelTime_fullRadius line 395
  34. lemma OAI.ExactSLEGreen.actual_physicalClock_mono line 405
  35. lemma OAI.ExactSLEGreen.levelTime_clock_le line 429
  36. lemma OAI.ExactSLEGreen.levelTime_clock_ge line 436
  37. abbrev OAI.ExactSLEGreen.PhaseVector line 449
  38. def OAI.ExactSLEGreen.phaseActive line 450
  39. def OAI.ExactSLEGreen.phaseSigma line 452
  40. def OAI.ExactSLEGreen.phaseOffset line 454
  41. def OAI.ExactSLEGreen.phaseConstant line 456
  42. def OAI.ExactSLEGreen.phaseProduct line 458