OAI/Probability/SLE/FiniteStoppedLaw.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Finite Stopped Law for chordal SLE.

  1. theorem OAI.SLEExactGauge.finite_stopped_green_regular line 17
  2. theorem OAI.SLEExactGauge.finite_stopped_green_of_witness line 97
  3. def OAI.SLEExactGauge.FiniteStoppedGreenTarget line 123
  4. theorem OAI.SLEExactGauge.finite_stopped_green line 139
  5. lemma OAI.SLEExactGauge.initialGreen_pos line 154
  6. lemma OAI.SLEExactGauge.greenDensity_nonneg line 162
  7. lemma OAI.SLEExactGauge.stoppedGreen_nonneg line 177
  8. def OAI.SLEExactGauge.finiteCenteredLaw line 188
  9. theorem OAI.SLEExactGauge.finiteCenteredLaw_probability line 195
  10. theorem OAI.SLEExactGauge.finiteCenteredLaw_live_compact line 214
  11. lemma OAI.SLEExactGauge.continuousOn_of_integral_balance line 252
  12. lemma OAI.SLEExactGauge.integral_drift_of_balance line 269
  13. def OAI.SLEExactGauge.radiusMoment line 318
  14. lemma OAI.SLEExactGauge.radiusMoment_nonneg line 322
  15. lemma OAI.SLEExactGauge.radiusMoment_intervalIntegrable line 327
  16. lemma OAI.SLEExactGauge.radiusMoment_intervalIntegral line 334
  17. lemma OAI.SLEExactGauge.balance_divide line 345
  18. lemma OAI.SLEExactGauge.radiusMoment_balance line 349
  19. theorem OAI.SLEExactGauge.radiusMoment_drift line 379
  20. def OAI.SLEExactGauge.stoppedInverseAngle line 422
  21. lemma OAI.SLEExactGauge.finiteCenteredLaw_inverseAngle_moment line 426
  22. lemma OAI.SLEExactGauge.limitRadiusKernel_zero_eq_indicator_level line 485
  23. lemma OAI.SLEExactGauge.integral_limitRadiusKernel_zero_eq_probability line 502
  24. lemma OAI.SLEExactGauge.initialGreen_div_zeroKernel line 532
  25. lemma OAI.SLEExactGauge.liminf_slope_of_integral_bound line 555
  26. lemma OAI.SLEExactGauge.image_le_of_integral_drift line 584
  27. def OAI.SLEExactGauge.lyapunovBarrier line 604
  28. lemma OAI.SLEExactGauge.lyapunovBarrier_pos line 606
  29. lemma OAI.SLEExactGauge.lyapunovBarrier_deriv line 609
  30. lemma OAI.SLEExactGauge.lyapunovBarrier_power line 617
  31. lemma OAI.SLEExactGauge.exists_small_barrier line 628
  32. theorem OAI.SLEExactGauge.comingDown_one_window line 638
  33. lemma OAI.SLEExactGauge.comingDown_shifted line 688
  34. theorem OAI.SLEExactGauge.comingDown_uniform line 707
  35. def OAI.SLEExactGauge.lyapunovA line 729
  36. def OAI.SLEExactGauge.lyapunovC line 730
  37. def OAI.SLEExactGauge.angularMomentBound line 731
  38. lemma OAI.SLEExactGauge.lyapunovA_nonneg line 734
  39. lemma OAI.SLEExactGauge.lyapunovC_pos line 736
  40. lemma OAI.SLEExactGauge.angularMomentBound_pos line 738
  41. theorem OAI.SLEExactGauge.radiusMoment_bound line 752
  42. lemma OAI.SLEExactGauge.limitRadiusKernel_antitone_power line 781
  43. lemma OAI.SLEExactGauge.integral_limitRadiusKernel_antitone_power line 792