OAI/Probability/SLELocalization/SwallowingLaws.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Swallowing estimates.

  1. lemma OAI.SLEExactGauge.Swallowing.generator_eq line 19
  2. lemma OAI.SLEExactGauge.Swallowing.radial_height_ineq line 42
  3. lemma OAI.SLEExactGauge.Swallowing.generator_negative line 56
  4. lemma OAI.SLEExactGauge.Swallowing.monomial_bound line 88
  5. lemma OAI.SLEExactGauge.Swallowing.radialX_bound line 102
  6. lemma OAI.SLEExactGauge.Swallowing.radialXX_bound line 111
  7. lemma OAI.SLEExactGauge.Swallowing.radialXXX_bound line 126
  8. lemma OAI.SLEExactGauge.Swallowing.deriv_lyapunov_driver line 154
  9. lemma OAI.SLEExactGauge.Swallowing.second_lyapunov_driver line 160
  10. lemma OAI.SLEExactGauge.Swallowing.third_lyapunov_driver line 172
  11. lemma OAI.SLEExactGauge.Swallowing.continuous_radial_comp line 183
  12. lemma OAI.SLEExactGauge.Swallowing.continuous_radialX_comp line 188
  13. lemma OAI.SLEExactGauge.Swallowing.continuous_radialXX_comp line 194
  14. def OAI.SLEExactGauge.Swallowing.field line 215
  15. def OAI.SLEExactGauge.Swallowing.drift line 218
  16. lemma OAI.SLEExactGauge.Swallowing.first_eq line 224
  17. lemma OAI.SLEExactGauge.Swallowing.second_eq line 230
  18. lemma OAI.SLEExactGauge.Swallowing.third_eq line 235
  19. lemma OAI.SLEExactGauge.Swallowing.smooth line 240
  20. lemma OAI.SLEExactGauge.Swallowing.coeff_uniform_bound line 244
  21. lemma OAI.SLEExactGauge.Swallowing.continuous_field line 262
  22. lemma OAI.SLEExactGauge.Swallowing.continuous_coeff line 272
  23. lemma OAI.SLEExactGauge.Swallowing.continuous_drift line 285
  24. lemma OAI.SLEExactGauge.Swallowing.time_deriv line 301
  25. lemma OAI.SLEExactGauge.Swallowing.regular line 319
  26. lemma OAI.SLEExactGauge.Swallowing.field_prefix_eq line 340
  27. def OAI.SLEExactGauge.BoundaryGreen.factor line 362
  28. def OAI.SLEExactGauge.BoundaryGreen.field line 365
  29. def OAI.SLEExactGauge.BoundaryGreen.drift line 368
  30. lemma OAI.SLEExactGauge.BoundaryGreen.factor_pos line 374
  31. lemma OAI.SLEExactGauge.BoundaryGreen.field_pos line 377
  32. lemma OAI.SLEExactGauge.BoundaryGreen.factor_bound line 381
  33. lemma OAI.SLEExactGauge.BoundaryGreen.first_eq line 387
  34. lemma OAI.SLEExactGauge.BoundaryGreen.second_eq line 396
  35. lemma OAI.SLEExactGauge.BoundaryGreen.third_eq line 407
  36. lemma OAI.SLEExactGauge.BoundaryGreen.smooth line 418
  37. lemma OAI.SLEExactGauge.BoundaryGreen.coeff_uniform_bound line 422
  38. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_factor line 448
  39. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_field line 452
  40. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_coeff line 460
  41. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_drift line 473
  42. lemma OAI.SLEExactGauge.BoundaryGreen.time_deriv line 486
  43. lemma OAI.SLEExactGauge.BoundaryGreen.field_prefix_eq line 498
  44. def OAI.SLEExactGauge.BoundaryGreen.gap line 507
  45. def OAI.SLEExactGauge.BoundaryGreen.weight line 510
  46. def OAI.SLEExactGauge.BoundaryGreen.deficit line 513
  47. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_gap line 516
  48. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_weight line 521
  49. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_deficit line 526
  50. lemma OAI.SLEExactGauge.BoundaryGreen.deficit_pos_iff line 531
  51. lemma OAI.SLEExactGauge.BoundaryGreen.deficit_nonneg_iff line 536
  52. def OAI.SLEExactGauge.BoundaryGreen.exitPath line 541
  53. def OAI.SLEExactGauge.BoundaryGreen.stop line 549
  54. lemma OAI.SLEExactGauge.BoundaryGreen.stop_bounds line 552
  55. lemma OAI.SLEExactGauge.BoundaryGreen.exitPath_extend line 557
  56. lemma OAI.SLEExactGauge.BoundaryGreen.exitPath_extend_div line 562
  57. lemma OAI.SLEExactGauge.BoundaryGreen.positive_before line 568
  58. lemma OAI.SLEExactGauge.BoundaryGreen.stop_pos line 575
  59. lemma OAI.SLEExactGauge.BoundaryGreen.nonneg_until line 580
  60. lemma OAI.SLEExactGauge.BoundaryGreen.nonpos_at_of_lt line 588
  61. lemma OAI.SLEExactGauge.BoundaryGreen.lt_stop_iff line 597
  62. lemma OAI.SLEExactGauge.BoundaryGreen.isOpen_positive_on line 616
  63. lemma OAI.SLEExactGauge.BoundaryGreen.deficit_prefix_eq line 638
  64. lemma OAI.SLEExactGauge.BoundaryGreen.regular line 646
  65. def OAI.SLEExactGauge.BoundaryGreen.coeffAt line 678
  66. lemma OAI.SLEExactGauge.BoundaryGreen.coeffAt_measurable line 684
  67. def OAI.SLEExactGauge.BoundaryGreen.rawCoeff line 699
  68. lemma OAI.SLEExactGauge.BoundaryGreen.rawCoeff_measurable_past line 703
  69. lemma OAI.SLEExactGauge.BoundaryGreen.rawCoeff_aemeasurable line 717
  70. lemma OAI.SLEExactGauge.BoundaryGreen.rawCoeff_eq line 731
  71. lemma OAI.SLEExactGauge.BoundaryGreen.rawCoeff_stoppedCoeff_ae line 754
  72. theorem OAI.SLEExactGauge.BoundaryGreen.localized_centered line 765
  73. def OAI.SLEExactGauge.BoundaryGreen.generator line 842
  74. lemma OAI.SLEExactGauge.BoundaryGreen.generator_factor line 845
  75. lemma OAI.SLEExactGauge.BoundaryGreen.generator_nonpos line 864
  76. lemma OAI.SLEExactGauge.BoundaryGreen.exponent_choice line 876
  77. lemma OAI.SLEExactGauge.BoundaryGreen.field_initial line 900
  78. lemma OAI.SLEExactGauge.BoundaryGreen.generator_field line 906