OAI/Probability/SLE/KernelExpectation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Kernel Expectation for chordal SLE.

  1. lemma OAI.SLEExactGauge.AngularLocalization.stopped_power_eq_kernel_of_hit line 19
  2. lemma OAI.SLEExactGauge.AngularLocalization.stopped_power_kernel_gap line 28
  3. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_region_integrable line 50
  4. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_region_integral line 65
  5. lemma OAI.SLEExactGauge.limitRadiusKernel_integrable line 88
  6. lemma OAI.SLEExactGauge.limitRadiusKernel_region_integrable line 103
  7. lemma OAI.SLEExactGauge.radiusKernel_region_integral_tendsto line 117
  8. lemma OAI.SLEExactGauge.stopped_power_tendsto_limitRadiusKernel line 142
  9. lemma OAI.SLEExactGauge.AngularLocalization.stopped_power_uniform_integrable line 179
  10. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_region_integral_eq_below line 191
  11. lemma OAI.SLEExactGauge.AngularLocalization.power_balance_below line 208
  12. lemma OAI.SLEExactGauge.stopped_power_integral_tendsto_limitRadiusKernel line 234
  13. theorem OAI.SLEExactGauge.limit_power_balance line 256
  14. lemma OAI.SLEExactGauge.AngularLocalization.radiusValue_factor line 329
  15. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_zero line 345
  16. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_power_factor line 353
  17. lemma OAI.SLEExactGauge.limitRadiusKernel_zero line 370
  18. lemma OAI.SLEExactGauge.limitRadiusKernel_zero_growth line 381
  19. lemma OAI.SLEExactGauge.limitRadiusKernel_power_factor line 397
  20. lemma OAI.SLEExactGauge.limitRadiusKernel_angle_le_one line 408
  21. lemma OAI.SLEExactGauge.integral_limitRadiusKernel_zero_growth line 414
  22. lemma OAI.SLEExactGauge.weighted_rpow_jensen line 438
  23. lemma OAI.SLEExactGauge.limitRadiusKernel_green_mean line 491
  24. lemma OAI.SLEExactGauge.limitRadiusKernel_inverse_factor line 509
  25. lemma OAI.SLEExactGauge.limitRadiusKernel_inverse_moment_jensen line 516
  26. def OAI.SLEExactGauge.AngularLocalization.weight line 558
  27. lemma OAI.SLEExactGauge.AngularLocalization.weight_bound line 561
  28. lemma OAI.SLEExactGauge.AngularLocalization.radius_at_hit line 566
  29. lemma OAI.SLEExactGauge.AngularLocalization.weight_eq_source line 578
  30. lemma OAI.SLEExactGauge.AngularLocalization.weight_eq_stoppedGreen_of_hit line 587
  31. lemma OAI.SLEExactGauge.AngularLocalization.weight_small_of_not_hit line 597
  32. lemma OAI.SLEExactGauge.eventually_hit_of_live_level line 610
  33. lemma OAI.SLEExactGauge.localizedRadiusStop_eq_source line 636
  34. lemma OAI.SLEExactGauge.localization_weight_tendsto line 659
  35. def OAI.SLEExactGauge.stoppedAngleSq line 695
  36. lemma OAI.SLEExactGauge.stoppedAngleSq_nonneg line 702
  37. lemma OAI.SLEExactGauge.radiusLevelTime_eq_top_of_no_level line 709
  38. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_zero_of_no_level line 721
  39. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_stopped_of_live_level line 735
  40. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_stoppedGreen line 751
  41. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_stoppedAngleSq line 767