OAI/Probability/SLE/AngularPowerDynkin.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Angular Power Dynkin for chordal SLE.

  1. lemma OAI.SLEExactGauge.powerLogGenerator_lyapunov line 15
  2. lemma OAI.SLEExactGauge.powerLogDensity_div_angle line 25
  3. lemma OAI.SLEExactGauge.powerLogGenerator_two_powers line 34
  4. theorem OAI.SLEExactGauge.AngularLocalization.mean_power line 54
  5. lemma OAI.SLEExactGauge.AngularLocalization.synchronize line 95
  6. lemma OAI.SLEExactGauge.AngularLocalization.stopping_le line 134
  7. lemma OAI.SLEExactGauge.AngularLocalization.hit_time_unique line 146
  8. lemma OAI.SLEExactGauge.AngularLocalization.hit_finer line 165
  9. lemma OAI.SLEExactGauge.continuous_logClockRate line 193
  10. lemma OAI.SLEExactGauge.AngularLocalization.radius_clock_derivative line 208
  11. def OAI.SLEExactGauge.AngularLocalization.clock line 218
  12. lemma OAI.SLEExactGauge.AngularLocalization.clock_measurable line 231
  13. lemma OAI.SLEExactGauge.AngularLocalization.inverse_measurable line 234
  14. lemma OAI.SLEExactGauge.AngularLocalization.clock_upper line 237
  15. def OAI.SLEExactGauge.AngularLocalization.radiusValue line 239
  16. lemma OAI.SLEExactGauge.AngularLocalization.radiusValue_continuous line 243
  17. lemma OAI.SLEExactGauge.AngularLocalization.radiusValue_measurable line 250
  18. lemma OAI.SLEExactGauge.AngularLocalization.radiusValue_at_clock line 257
  19. lemma OAI.SLEExactGauge.AngularLocalization.radius_integral_substitution line 264
  20. lemma OAI.SLEExactGauge.powerLogDensity_le_radius_angle line 302
  21. def OAI.SLEExactGauge.AngularLocalization.radiusKernel line 324
  22. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_nonneg line 327
  23. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_le line 333
  24. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_measurable line 345
  25. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_integral line 353
  26. lemma OAI.SLEExactGauge.AngularLocalization.synchronize_real line 360
  27. lemma OAI.SLEExactGauge.AngularLocalization.terminal_clock_le line 366
  28. lemma OAI.SLEExactGauge.AngularLocalization.inverse_synchronize line 376
  29. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_mono line 391
  30. lemma OAI.SLEExactGauge.AngularLocalization.physical_power_continuous line 421
  31. lemma OAI.SLEExactGauge.AngularLocalization.generator_radial_integral line 430
  32. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_cumulative_integrable line 458
  33. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_fubini line 474
  34. theorem OAI.SLEExactGauge.AngularLocalization.power_balance line 493
  35. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_eq_of_live line 532
  36. lemma OAI.SLEExactGauge.AngularLocalization.terminal_clock_min line 544
  37. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_eq_below line 563
  38. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_uniform_bound line 574
  39. def OAI.SLEExactGauge.limitRadiusKernel line 593
  40. lemma OAI.SLEExactGauge.radiusKernel_eventually_limit line 598
  41. lemma OAI.SLEExactGauge.limitRadiusKernel_nonneg line 612
  42. lemma OAI.SLEExactGauge.limitRadiusKernel_measurable line 620
  43. lemma OAI.SLEExactGauge.limitRadiusKernel_uniform_bound line 633
  44. def OAI.SLEExactGauge.AngularLocalization.hit line 656
  45. lemma OAI.SLEExactGauge.AngularLocalization.measurable_hit line 659
  46. def OAI.SLEExactGauge.AngularLocalization.hitTime line 663
  47. lemma OAI.SLEExactGauge.AngularLocalization.hitTime_stopping line 666
  48. def OAI.SLEExactGauge.localizedRadiusStop line 687
  49. lemma OAI.SLEExactGauge.localizedRadiusStop_eq_hit line 691
  50. lemma OAI.SLEExactGauge.localizedRadiusStop_eq_top line 704
  51. lemma OAI.SLEExactGauge.localizedRadiusStop_le_iff line 709
  52. lemma OAI.SLEExactGauge.localizedRadiusStop_stopping line 724
  53. lemma OAI.SLEExactGauge.localizedRadiusStop_history_hit line 737
  54. lemma OAI.SLEExactGauge.integrable_monotone_limit_of_integral_le line 767