OAI/Probability/SLELocalization/GreenTilts.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Loewner Localized estimates.

  1. lemma OAI.SLEExactGauge.LoewnerLocalized.source_until_stop line 41
  2. lemma OAI.SLEExactGauge.LoewnerLocalized.logDerivative_eq_source line 58
  3. lemma OAI.SLEExactGauge.LoewnerLocalized.radius_eq_source line 83
  4. lemma OAI.SLEExactGauge.LoewnerLocalized.sine_eq_source line 96
  5. lemma OAI.SLEExactGauge.LoewnerLocalized.field_eq_radius_sine line 159
  6. lemma OAI.SLEExactGauge.LoewnerLocalized.clock_bounds_stop line 170
  7. lemma OAI.SLEExactGauge.LoewnerLocalized.terminal_cases line 201
  8. structure OAI.SLEExactGauge.FiniteTilt.Cutoff line 276
  9. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.height_initial line 338
  10. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.initial_deficit line 343
  11. def OAI.SLEExactGauge.FiniteTilt.Cutoff.paths line 358
  12. def OAI.SLEExactGauge.FiniteTilt.Cutoff.stopTime line 361
  13. def OAI.SLEExactGauge.FiniteTilt.Cutoff.value line 364
  14. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.path_eq line 368
  15. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.initial_deficit_brownian line 375
  16. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.bounds line 384
  17. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.value_nonneg line 388
  18. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.value_bound line 391
  19. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.expectation line 405
  20. lemma OAI.SLEExactGauge.FiniteTilt.initial_sine_pos line 462
  21. def OAI.SLEExactGauge.FiniteTilt.shrinkingAngle line 469
  22. lemma OAI.SLEExactGauge.FiniteTilt.shrinkingAngle_pos line 471
  23. lemma OAI.SLEExactGauge.FiniteTilt.shrinkingAngle_initial line 474
  24. lemma OAI.SLEExactGauge.FiniteTilt.shrinkingAngle_tendsto line 480
  25. def OAI.SLEExactGauge.FiniteTilt.cutoffs line 485
  26. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.source_live line 556
  27. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.source_radius line 560
  28. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.source_sine line 567
  29. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.radius_lower line 575
  30. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.value_eq_source line 581
  31. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.source_terminal line 591
  32. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.stopTime_le_radius line 601
  33. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.angle_exit_bound line 612
  34. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.sine_positive_minimum line 668
  35. lemma OAI.SLEExactGauge.FiniteTilt.eventually_value_at_radius line 743
  36. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_value_killed line 769
  37. lemma OAI.SLEExactGauge.finiteStoppedDensity_zero line 852
  38. lemma OAI.SLEExactGauge.green_initial line 862
  39. theorem OAI.SLEExactGauge.finiteStoppedCenteredLaw line 870
  40. def OAI.SLEExactGauge.BoundaryFunctional.clampRe line 939
  41. def OAI.SLEExactGauge.BoundaryFunctional.velocity line 941
  42. lemma OAI.SLEExactGauge.BoundaryFunctional.clampRe_ne_zero line 943
  43. lemma OAI.SLEExactGauge.BoundaryFunctional.clampRe_norm line 946
  44. lemma OAI.SLEExactGauge.BoundaryFunctional.clampRe_norm_sub line 949
  45. lemma OAI.SLEExactGauge.BoundaryFunctional.velocity_lipschitz line 952
  46. lemma OAI.SLEExactGauge.BoundaryFunctional.norm_velocity_sub_le line 956
  47. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_velocity line 960
  48. lemma OAI.SLEExactGauge.BoundaryFunctional.exists_solution line 964
  49. lemma OAI.SLEExactGauge.BoundaryFunctional.norm_velocity_driver_sub_le line 970
  50. lemma OAI.SLEExactGauge.BoundaryFunctional.derivWithin_right line 980
  51. lemma OAI.SLEExactGauge.BoundaryFunctional.derivWithin_left line 986
  52. lemma OAI.SLEExactGauge.BoundaryFunctional.solution_eq line 992
  53. lemma OAI.SLEExactGauge.BoundaryFunctional.solution_dist_le line 1002
  54. def OAI.SLEExactGauge.BoundaryFunctional.extendDriver line 1051
  55. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_extendDriver line 1054
  56. def OAI.SLEExactGauge.BoundaryFunctional.solution line 1057
  57. lemma OAI.SLEExactGauge.BoundaryFunctional.solution_initial line 1060
  58. lemma OAI.SLEExactGauge.BoundaryFunctional.solution_deriv line 1065
  59. def OAI.SLEExactGauge.BoundaryFunctional.solutionPath line 1071
  60. lemma OAI.SLEExactGauge.BoundaryFunctional.solutionPath_lipschitz line 1076
  61. def OAI.SLEExactGauge.BoundaryFunctional.position line 1095
  62. lemma OAI.SLEExactGauge.BoundaryFunctional.position_eq line 1099
  63. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_position line 1106
  64. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_joint_extendDriver line 1111
  65. def OAI.SLEExactGauge.BoundaryFunctional.variation line 1116
  66. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_clampRe line 1120
  67. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_variation line 1125
  68. def OAI.SLEExactGauge.BoundaryFunctional.logDerivative line 1133
  69. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_logDerivative line 1137
  70. lemma OAI.SLEExactGauge.BoundaryFunctional.abs_variation_le line 1145
  71. lemma OAI.SLEExactGauge.BoundaryFunctional.logDerivative_initial line 1153
  72. lemma OAI.SLEExactGauge.BoundaryFunctional.abs_logDerivative_le line 1157
  73. lemma OAI.SLEExactGauge.BoundaryFunctional.position_initial line 1170
  74. lemma OAI.SLEExactGauge.BoundaryFunctional.position_derivWithin line 1174
  75. lemma OAI.SLEExactGauge.BoundaryFunctional.position_deriv line 1182
  76. lemma OAI.SLEExactGauge.BoundaryFunctional.logDerivative_eq_integral line 1188
  77. lemma OAI.SLEExactGauge.BoundaryFunctional.hasDerivAt_logDerivative line 1193
  78. lemma OAI.SLEExactGauge.BoundaryFunctional.position_prefix_eq line 1207
  79. lemma OAI.SLEExactGauge.BoundaryFunctional.logDerivative_prefix_eq line 1221
  80. lemma OAI.SLEExactGauge.BoundaryFunctional.position_im_zero line 1236
  81. def OAI.SLEExactGauge.Swallowing.radial line 1262
  82. def OAI.SLEExactGauge.Swallowing.lyapunov line 1264
  83. def OAI.SLEExactGauge.Swallowing.radialX line 1266
  84. def OAI.SLEExactGauge.Swallowing.radialXX line 1268
  85. def OAI.SLEExactGauge.Swallowing.radialXXX line 1271
  86. lemma OAI.SLEExactGauge.Swallowing.radial_pos line 1275
  87. lemma OAI.SLEExactGauge.Swallowing.hasDerivAt_radial_path line 1278
  88. lemma OAI.SLEExactGauge.Swallowing.hasDerivAt_radial_x line 1287
  89. lemma OAI.SLEExactGauge.Swallowing.hasDerivAt_radialX_x line 1292
  90. lemma OAI.SLEExactGauge.Swallowing.hasDerivAt_radialXX_x line 1304
  91. lemma OAI.SLEExactGauge.Swallowing.contDiff_radial_driver line 1315
  92. lemma OAI.SLEExactGauge.Swallowing.lyapunov_nonneg line 1322
  93. def OAI.SLEExactGauge.Swallowing.generator line 1326