OAI/Probability/SLE/WindowBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Window Bounds for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_liveTime_eq_sphere_of_finite line 17
  2. lemma OAI.SLEExactGauge.source_windowV_stopped_eq line 25
  3. lemma OAI.SLEExactGauge.source_windowV_stopped_measurable line 43
  4. lemma OAI.SLEExactGauge.source_liveWeight_stopped_measurable line 61
  5. lemma OAI.SLEExactGauge.source_collarHB_joint line 81
  6. lemma OAI.SLEExactGauge.source_stop_space_congr line 117
  7. lemma OAI.SLEExactGauge.source_collarHBV_stopped line 124
  8. lemma OAI.SLEExactGauge.source_collarWeight_stopped line 146
  9. theorem OAI.SLEExactGauge.sourceSpatialWindowMeasurable_proved line 162
  10. lemma OAI.SLEExactGauge.source_liveIndicator_measurable line 187
  11. def OAI.SLEExactGauge.sourceApproachConstant line 242
  12. lemma OAI.SLEExactGauge.sourceApproachConstant_pos line 246
  13. lemma OAI.SLEExactGauge.source_kernel_mean_bound line 251
  14. lemma OAI.SLEExactGauge.source_liveSpatialHitTime_ne_top_iff line 337
  15. lemma OAI.SLEExactGauge.source_live_contact_restarts line 349
  16. lemma OAI.SLEExactGauge.source_liveIndicator_zero_of_coarse_top line 393
  17. lemma OAI.SLEExactGauge.source_restarted_kernel_dominates line 409
  18. lemma OAI.SLEExactGauge.source_stopped_kernel_mean_bound line 433
  19. lemma OAI.SLEExactGauge.source_finite_approach_setIntegral_bound line 479
  20. def OAI.SLEExactGauge.SourceConditionalApproachTarget line 598
  21. lemma OAI.SLEExactGauge.source_approach_small_scale line 611
  22. theorem OAI.SLEExactGauge.sourceConditionalApproach_proved line 634