OAI/Probability/SLE/RectangleMeans.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Rectangle Means for chordal SLE.

  1. def OAI.SLEExactGauge.cellOrigin line 13
  2. def OAI.SLEExactGauge.dyadicCell line 14
  3. def OAI.SLEExactGauge.dyadicInterior line 16
  4. lemma OAI.SLEExactGauge.dyadicCell_eq line 19
  5. lemma OAI.SLEExactGauge.cellOrigin_nonneg line 22
  6. lemma OAI.SLEExactGauge.cellOrigin_right line 24
  7. lemma OAI.SLEExactGauge.dyadicInterior_subset_unit line 30
  8. lemma OAI.SLEExactGauge.dyadicCell_subset_root line 40
  9. lemma OAI.SLEExactGauge.cellOrigin_separated line 52
  10. lemma OAI.SLEExactGauge.dyadicInterior_disjoint line 59
  11. def OAI.SLEExactGauge.leftChild line 77
  12. def OAI.SLEExactGauge.rightChild line 79
  13. lemma OAI.SLEExactGauge.cellOrigin_leftChild line 81
  14. lemma OAI.SLEExactGauge.cellOrigin_rightChild line 85
  15. def OAI.SLEExactGauge.branchIndex line 91
  16. lemma OAI.SLEExactGauge.branchIndex_step line 96
  17. lemma OAI.SLEExactGauge.branchIndex_contains line 109
  18. def OAI.SLEExactGauge.pointBranch line 122
  19. lemma OAI.SLEExactGauge.pointBranch_contains line 124
  20. lemma OAI.SLEExactGauge.stripRectangle_convex line 139
  21. lemma OAI.SLEExactGauge.stripRectangle_compact line 150
  22. lemma OAI.SLEExactGauge.stripRectangle_nonempty line 156
  23. lemma OAI.SLEExactGauge.spatialAverage_eq_setAverage line 162
  24. lemma OAI.SLEExactGauge.stripRectangle_average_attained line 167
  25. lemma OAI.SLEExactGauge.dyadicCell_dist_le line 179
  26. lemma OAI.SLEExactGauge.scaleLength_tendsto line 191
  27. lemma OAI.SLEExactGauge.branch_means_tendsto line 197
  28. def OAI.SLEExactGauge.cellEnergy line 214
  29. lemma OAI.SLEExactGauge.cellEnergy_nonneg line 216
  30. lemma OAI.SLEExactGauge.branch_mean_step_le line 219
  31. lemma OAI.SLEExactGauge.sum_cellEnergy_le line 238
  32. lemma OAI.SLEExactGauge.exists_large_increment line 254
  33. lemma OAI.SLEExactGauge.large_increment_energy line 276
  34. def OAI.SLEExactGauge.exceptionalParents line 289
  35. lemma OAI.SLEExactGauge.mem_exceptionalParents line 294
  36. lemma OAI.SLEExactGauge.exceptional_cover line 300
  37. lemma OAI.SLEExactGauge.exceptional_count line 320
  38. def OAI.SLEExactGauge.polyGeometricSum line 345
  39. lemma OAI.SLEExactGauge.summable_polyGeometric line 347
  40. lemma OAI.SLEExactGauge.polyGeometricSum_pos line 359
  41. lemma OAI.SLEExactGauge.decay_factor line 365
  42. lemma OAI.SLEExactGauge.summable_weighted_decay line 371
  43. lemma OAI.SLEExactGauge.tsum_weighted_decay line 381
  44. lemma OAI.SLEExactGauge.finite_union_hit_bound line 393
  45. lemma OAI.SLEExactGauge.rectangle_bound_at_depth line 404
  46. def OAI.SLEExactGauge.energyDepth line 448
  47. lemma OAI.SLEExactGauge.energyDepth_mean_bound line 450
  48. lemma OAI.SLEExactGauge.energyDepth_lower line 462
  49. lemma OAI.SLEExactGauge.energyDepth_decay line 473
  50. def OAI.SLEExactGauge.SourceStripRectangleEnergyTarget line 489
  51. lemma OAI.SLEExactGauge.critical_cell_means_le line 506
  52. lemma OAI.SLEExactGauge.high_set_empty_of_energy_zero line 521
  53. theorem OAI.SLEExactGauge.sourceStripRectangleEnergy line 538
  54. lemma OAI.SLEExactGauge.source_local_lipschitz_weak_derivative line 572
  55. lemma OAI.SLEExactGauge.real_gradient_re line 624
  56. lemma OAI.SLEExactGauge.real_gradient_im line 629
  57. lemma OAI.SLEExactGauge.locallyLipschitz_source_weakGradient line 634