OAI/Probability/SLE/StripKernels.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Strip Kernels for chordal SLE.

  1. lemma OAI.SLEExactGauge.integrable_mul_compact_test line 13
  2. lemma OAI.SLEExactGauge.weak_gradient_pairing line 20
  3. lemma OAI.SLEExactGauge.complex_pairing_abs_le line 42
  4. lemma OAI.SLEExactGauge.integral_nonneg_cauchy line 52
  5. lemma OAI.SLEExactGauge.integral_pairing_le line 62
  6. def OAI.SLEExactGauge.chainDensity line 84
  7. def OAI.SLEExactGauge.chainX line 88
  8. def OAI.SLEExactGauge.chainY line 93
  9. def OAI.SLEExactGauge.chainKernel line 98
  10. lemma OAI.SLEExactGauge.chainX_smooth line 101
  11. lemma OAI.SLEExactGauge.chainY_smooth line 103
  12. lemma OAI.SLEExactGauge.chainX_compact line 105
  13. lemma OAI.SLEExactGauge.chainY_compact line 109
  14. lemma OAI.SLEExactGauge.chainX_support line 116
  15. lemma OAI.SLEExactGauge.chainY_support line 135
  16. lemma OAI.SLEExactGauge.chain_divergence line 153
  17. lemma OAI.SLEExactGauge.chainKernel_continuous line 160
  18. lemma OAI.SLEExactGauge.chainKernel_compact line 162
  19. lemma OAI.SLEExactGauge.chainKernel_nonneg line 166
  20. lemma OAI.SLEExactGauge.chainKernel_bound line 169
  21. lemma OAI.SLEExactGauge.chainKernel_integral_bound line 189
  22. lemma OAI.SLEExactGauge.compact_sum_range line 217
  23. lemma OAI.SLEExactGauge.support_sum_range line 225
  24. def OAI.SLEExactGauge.aggregateX line 234
  25. def OAI.SLEExactGauge.aggregateY line 236
  26. lemma OAI.SLEExactGauge.aggregateX_smooth line 239
  27. lemma OAI.SLEExactGauge.aggregateY_smooth line 241
  28. lemma OAI.SLEExactGauge.aggregateX_compact line 243
  29. lemma OAI.SLEExactGauge.aggregateY_compact line 246
  30. lemma OAI.SLEExactGauge.aggregateX_support line 249
  31. lemma OAI.SLEExactGauge.aggregateY_support line 253
  32. lemma OAI.SLEExactGauge.aggregate_divergence line 258
  33. lemma OAI.SLEExactGauge.aggregate_kernel_bound line 268
  34. lemma OAI.SLEExactGauge.chainDensity_continuous line 307
  35. lemma OAI.SLEExactGauge.chainDensity_compact line 309
  36. lemma OAI.SLEExactGauge.smoothed_means_le line 312
  37. def OAI.SLEExactGauge.stripRectangle line 344
  38. lemma OAI.SLEExactGauge.stripRectangle_eq_preimage line 347
  39. lemma OAI.SLEExactGauge.stripRectangle_volume line 355
  40. lemma OAI.SLEExactGauge.stripRectangle_integral_mul line 363
  41. lemma OAI.SLEExactGauge.stripRectangle_integral_re line 377
  42. def OAI.SLEExactGauge.spatialAverage line 389
  43. def OAI.SLEExactGauge.openStripRectangle line 392
  44. lemma OAI.SLEExactGauge.openStripRectangle_eq_preimage line 395
  45. lemma OAI.SLEExactGauge.openStripRectangle_measurable line 403
  46. lemma OAI.SLEExactGauge.openStripRectangle_ae_eq line 408
  47. lemma OAI.SLEExactGauge.rectangleDensity_nonneg line 415
  48. lemma OAI.SLEExactGauge.rectangleDensity_bound line 418
  49. lemma OAI.SLEExactGauge.rectangleDensity_tendsto line 425
  50. lemma OAI.SLEExactGauge.rectangle_smoothed_mean_tendsto line 445
  51. def OAI.SLEExactGauge.dyadicStripRectangle line 482
  52. def OAI.SLEExactGauge.SourceCriticalStripMeansTarget line 488
  53. lemma OAI.SLEExactGauge.chain_means_le line 496
  54. theorem OAI.SLEExactGauge.sourceCriticalStripMeans line 515
  55. lemma OAI.SLEExactGauge.integral_pairing_local_le line 529
  56. lemma OAI.SLEExactGauge.rectangle_transport_L2_bound line 561
  57. lemma OAI.SLEExactGauge.openStripRectangle_subset_unit line 608
  58. lemma OAI.SLEExactGauge.local_means_le line 615