OAI/Probability/SLE/OccupationBound.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Occupation Bound for chordal SLE.

  1. lemma OAI.SLEExactGauge.occupation_difference line 15
  2. lemma OAI.SLEExactGauge.high_occupation_le line 27
  3. lemma OAI.SLEExactGauge.point_le_occupation line 46
  4. lemma OAI.SLEExactGauge.radiusMoment_zero_growth line 68
  5. lemma OAI.SLEExactGauge.radiusMoment_zero_le_high line 80
  6. lemma OAI.SLEExactGauge.radiusMoment_high_integrable line 93
  7. lemma OAI.SLEExactGauge.radiusMoment_high_occupation line 106
  8. def OAI.SLEExactGauge.inverseAngleBound line 141
  9. lemma OAI.SLEExactGauge.inverseAngleBound_pos line 145
  10. lemma OAI.SLEExactGauge.radiusMoment_zero_growth_high_ae line 157
  11. theorem OAI.SLEExactGauge.radiusMoment_inverseAngle_bound line 186
  12. lemma OAI.SLEExactGauge.localization_integral_tendsto line 231
  13. lemma OAI.SLEExactGauge.localization_history_finer line 250
  14. lemma OAI.SLEExactGauge.finite_history_on_hit line 264
  15. lemma OAI.SLEExactGauge.hit_integral_tendsto line 287
  16. theorem OAI.SLEExactGauge.finite_stopped_green_consistent_regular line 317
  17. lemma OAI.SLEExactGauge.finiteCenteredLaw_apply line 361
  18. theorem OAI.SLEExactGauge.exists_consistent_finiteCenteredLaw_regular line 381
  19. lemma OAI.SLEExactGauge.finiteCenteredLaw_congr_driver line 426
  20. theorem OAI.SLEExactGauge.exists_consistent_finiteCenteredLaw line 437
  21. def OAI.SLEExactGauge.inverseAngleSubcritical line 478
  22. def OAI.SLEExactGauge.inverseAngleBuffer line 480
  23. def OAI.SLEExactGauge.uniformInverseAngleConstant line 481
  24. lemma OAI.SLEExactGauge.inverseAngleSubcritical_bounds line 484
  25. lemma OAI.SLEExactGauge.uniformInverseAngleConstant_pos line 496
  26. theorem OAI.SLEExactGauge.uniform_inverse_angle_regular line 503
  27. theorem OAI.SLEExactGauge.uniform_inverse_angle line 546
  28. lemma OAI.SLEExactGauge.radius_approach_regular line 584
  29. theorem OAI.SLEExactGauge.radius_approach line 631
  30. theorem OAI.SLEExactGauge.euclidean_approach_at_level line 661
  31. theorem OAI.SLEExactGauge.euclidean_approach line 686