OAI/Probability/SLELocalization/StoppedIto.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Brownian Stopped estimates.

  1. theorem OAI.SLEExactGauge.BrownianStopped.stopped_fieldSum_tendsto_ae line 28
  2. theorem OAI.SLEExactGauge.BrownianStopped.stopped_field_ito_centered_ae line 103
  3. def OAI.SLEExactGauge.LoewnerCutoff.clampIm line 168
  4. def OAI.SLEExactGauge.LoewnerCutoff.velocity line 170
  5. lemma OAI.SLEExactGauge.LoewnerCutoff.clampIm_eq line 172
  6. lemma OAI.SLEExactGauge.LoewnerCutoff.clampIm_height line 175
  7. lemma OAI.SLEExactGauge.LoewnerCutoff.clampIm_norm line 177
  8. lemma OAI.SLEExactGauge.LoewnerCutoff.clampIm_ne_zero line 180
  9. lemma OAI.SLEExactGauge.LoewnerCutoff.clampIm_norm_sub line 183
  10. lemma OAI.SLEExactGauge.LoewnerCutoff.velocity_eq line 196
  11. lemma OAI.SLEExactGauge.LoewnerCutoff.norm_velocity_le line 201
  12. lemma OAI.SLEExactGauge.LoewnerCutoff.norm_velocity_sub_le line 206
  13. lemma OAI.SLEExactGauge.LoewnerCutoff.velocity_lipschitz line 230
  14. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_velocity line 237
  15. lemma OAI.SLEExactGauge.LoewnerCutoff.exists_solution line 246
  16. lemma OAI.SLEExactGauge.LoewnerCutoff.norm_velocity_driver_sub_le line 268
  17. lemma OAI.SLEExactGauge.LoewnerCutoff.derivWithin_right line 278
  18. lemma OAI.SLEExactGauge.LoewnerCutoff.derivWithin_left line 284
  19. lemma OAI.SLEExactGauge.LoewnerCutoff.solution_eq line 290
  20. lemma OAI.SLEExactGauge.LoewnerCutoff.solution_dist_le line 300
  21. def OAI.SLEExactGauge.LoewnerCutoff.extendDriver line 369
  22. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_extendDriver line 372
  23. def OAI.SLEExactGauge.LoewnerCutoff.solution line 375
  24. lemma OAI.SLEExactGauge.LoewnerCutoff.solution_initial line 378
  25. lemma OAI.SLEExactGauge.LoewnerCutoff.solution_deriv line 383
  26. def OAI.SLEExactGauge.LoewnerCutoff.solutionPath line 389
  27. lemma OAI.SLEExactGauge.LoewnerCutoff.solutionPath_lipschitz line 394
  28. def OAI.SLEExactGauge.ContinuousDriver.selectedLimit line 450
  29. lemma OAI.SLEExactGauge.ContinuousDriver.tendsto_selectedLimit line 454
  30. lemma OAI.SLEExactGauge.ContinuousDriver.selectedLimit_eq line 459
  31. lemma OAI.SLEExactGauge.ContinuousDriver.measurableSet_cauchy line 506
  32. lemma OAI.SLEExactGauge.ContinuousDriver.measurable_selectedLimit line 515
  33. def OAI.SLEExactGauge.ContinuousDriver.rawApprox line 568
  34. lemma OAI.SLEExactGauge.ContinuousDriver.rawApprox_eq line 571
  35. lemma OAI.SLEExactGauge.ContinuousDriver.measurable_rawApprox line 576
  36. def OAI.SLEExactGauge.ContinuousDriver.path line 585
  37. lemma OAI.SLEExactGauge.ContinuousDriver.path_eq line 587
  38. lemma OAI.SLEExactGauge.ContinuousDriver.path_eval_of_continuous line 594
  39. lemma OAI.SLEExactGauge.ContinuousDriver.measurable_path line 598
  40. def OAI.SLEExactGauge.LoewnerCutoff.position line 643
  41. lemma OAI.SLEExactGauge.LoewnerCutoff.position_eq line 647
  42. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_position line 654
  43. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_joint_extendDriver line 659
  44. def OAI.SLEExactGauge.LoewnerCutoff.variation line 664
  45. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_clampIm line 668
  46. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_variation line 673
  47. def OAI.SLEExactGauge.LoewnerCutoff.logDerivative line 681
  48. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_logDerivative line 685
  49. lemma OAI.SLEExactGauge.LoewnerCutoff.abs_variation_le line 693
  50. lemma OAI.SLEExactGauge.LoewnerCutoff.logDerivative_initial line 701
  51. lemma OAI.SLEExactGauge.LoewnerCutoff.abs_logDerivative_le line 705
  52. lemma OAI.SLEExactGauge.LoewnerCutoff.position_initial line 718
  53. lemma OAI.SLEExactGauge.LoewnerCutoff.position_derivWithin line 722
  54. lemma OAI.SLEExactGauge.LoewnerCutoff.position_deriv line 730
  55. lemma OAI.SLEExactGauge.LoewnerCutoff.logDerivative_eq_integral line 736
  56. lemma OAI.SLEExactGauge.LoewnerCutoff.hasDerivAt_logDerivative line 741
  57. lemma OAI.SLEExactGauge.LoewnerCutoff.position_prefix_eq line 755
  58. lemma OAI.SLEExactGauge.LoewnerCutoff.logDerivative_prefix_eq line 769
  59. def OAI.SLEExactGauge.GreenPhysical.green line 824
  60. lemma OAI.SLEExactGauge.GreenPhysical.q_pos line 827
  61. lemma OAI.SLEExactGauge.GreenPhysical.green_eq_source line 829
  62. lemma OAI.SLEExactGauge.GreenPhysical.green_pos line 843
  63. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_green_path line 845
  64. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_green_x line 859
  65. lemma OAI.SLEExactGauge.GreenPhysical.deriv_green_x line 864
  66. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_neg_ax_div_q line 868
  67. lemma OAI.SLEExactGauge.GreenPhysical.deriv_deriv_green_x line 878
  68. lemma OAI.SLEExactGauge.GreenPhysical.green_drift_cancellation line 892
  69. lemma OAI.SLEExactGauge.GreenPhysical.loewner_green_drift line 903
  70. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_green_driver line 918
  71. lemma OAI.SLEExactGauge.GreenPhysical.deriv_green_driver line 926
  72. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_deriv_green_x line 931
  73. lemma OAI.SLEExactGauge.GreenPhysical.deriv_deriv_green_driver line 942
  74. lemma OAI.SLEExactGauge.GreenPhysical.green_le_radius line 958
  75. lemma OAI.SLEExactGauge.GreenPhysical.green_le_fixed_radius line 970
  76. lemma OAI.SLEExactGauge.GreenPhysical.contDiff_green_x line 976
  77. lemma OAI.SLEExactGauge.GreenPhysical.contDiff_green_driver line 984
  78. lemma OAI.SLEExactGauge.GreenPhysical.hasDerivAt_second_green_x line 988
  79. lemma OAI.SLEExactGauge.GreenPhysical.third_green_x line 1003
  80. lemma OAI.SLEExactGauge.GreenPhysical.iteratedDeriv_green_driver line 1009
  81. lemma OAI.SLEExactGauge.GreenPhysical.abs_x_div_q_le line 1027
  82. lemma OAI.SLEExactGauge.GreenPhysical.inv_q_le line 1034
  83. lemma OAI.SLEExactGauge.GreenPhysical.third_green_bound line 1039
  84. lemma OAI.SLEExactGauge.GreenPhysical.continuous_green_comp line 1065
  85. lemma OAI.SLEExactGauge.GreenPhysical.first_green_bound line 1076
  86. lemma OAI.SLEExactGauge.GreenPhysical.second_green_bound line 1090
  87. def OAI.SLEExactGauge.LoewnerField.height line 1155
  88. def OAI.SLEExactGauge.LoewnerField.field line 1158
  89. def OAI.SLEExactGauge.LoewnerField.drift line 1162