OAI/Probability/SLE/WindowGeometry.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Window Geometry for chordal SLE.

  1. def OAI.SLEExactGauge.sourceSpatialWindowSet line 16
  2. def OAI.SLEExactGauge.sourceSpatialWindowTime line 19
  3. def OAI.SLEExactGauge.sourceSpatialWindowH line 22
  4. def OAI.SLEExactGauge.sourceSpatialWindowB line 26
  5. def OAI.SLEExactGauge.SourceSpatialWindowGeometryTarget line 33
  6. lemma OAI.SLEExactGauge.source_liveHit_mem line 56
  7. lemma OAI.SLEExactGauge.source_liveHit_le line 68
  8. lemma OAI.SLEExactGauge.source_liveHit_antitone line 75
  9. lemma OAI.SLEExactGauge.source_windowSet_closed line 85
  10. lemma OAI.SLEExactGauge.source_window_le_of_mem line 96
  11. lemma OAI.SLEExactGauge.source_window_mem line 103
  12. lemma OAI.SLEExactGauge.source_window_start_le line 114
  13. lemma OAI.SLEExactGauge.source_before_window line 123
  14. lemma OAI.SLEExactGauge.source_window_le_fine line 133
  15. lemma OAI.SLEExactGauge.source_windowH_iff line 144
  16. lemma OAI.SLEExactGauge.source_windowB_before line 168
  17. lemma OAI.SLEExactGauge.source_window_missed line 187
  18. theorem OAI.SLEExactGauge.sourceSpatialWindowGeometry_proved line 216
  19. def OAI.SLEExactGauge.sourceCollarStart line 279
  20. def OAI.SLEExactGauge.sourceCollarFinish line 281
  21. def OAI.SLEExactGauge.sourceCollarH line 283
  22. def OAI.SLEExactGauge.sourceCollarB line 285
  23. def OAI.SLEExactGauge.SourceSpatialWindowMeasurableTarget line 289
  24. lemma OAI.SLEExactGauge.source_window_le_iff line 314
  25. lemma OAI.SLEExactGauge.source_liveTime_eq_killed line 326
  26. lemma OAI.SLEExactGauge.source_live_stopped_measurable line 338
  27. lemma OAI.SLEExactGauge.source_liveHit_stopping line 359
  28. lemma OAI.SLEExactGauge.source_windowKernel_closed line 385
  29. lemma OAI.SLEExactGauge.source_min_time_coe line 409
  30. lemma OAI.SLEExactGauge.source_window_kernel_iff line 415
  31. def OAI.SLEExactGauge.sourceCapPath line 435
  32. lemma OAI.SLEExactGauge.source_cap_domain line 438
  33. lemma OAI.SLEExactGauge.source_window_kernel_cap line 447
  34. lemma OAI.SLEExactGauge.source_tracePath_measurable line 461
  35. lemma OAI.SLEExactGauge.source_capPath_adapted line 469
  36. lemma OAI.SLEExactGauge.source_window_stopping line 478
  37. lemma OAI.SLEExactGauge.source_collarStart_stopping line 506
  38. lemma OAI.SLEExactGauge.source_collarFinish_stopping line 515
  39. lemma OAI.SLEExactGauge.source_joint_survival_measurable line 524
  40. lemma OAI.SLEExactGauge.source_collarStart_joint line 530
  41. lemma OAI.SLEExactGauge.source_collarFinish_joint line 557
  42. lemma OAI.SLEExactGauge.source_spatialWeight_stopping_measurable line 592
  43. lemma OAI.SLEExactGauge.source_windowH_untopA line 619
  44. lemma OAI.SLEExactGauge.source_windowB_untopA line 631
  45. lemma OAI.SLEExactGauge.source_windowHB_stopped_measurable line 643