OAI/Probability/SLELocalization/LoewnerFlow.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Loewner Field estimates.

  1. lemma OAI.SLEExactGauge.LoewnerField.height_pos line 39
  2. lemma OAI.SLEExactGauge.LoewnerField.smooth line 42
  3. lemma OAI.SLEExactGauge.LoewnerField.continuous_field line 46
  4. lemma OAI.SLEExactGauge.LoewnerField.continuous_drift line 57
  5. lemma OAI.SLEExactGauge.LoewnerField.field_upper line 77
  6. lemma OAI.SLEExactGauge.LoewnerField.field_third_bound line 89
  7. lemma OAI.SLEExactGauge.LoewnerField.time_deriv line 102
  8. lemma OAI.SLEExactGauge.LoewnerField.second_eq line 118
  9. lemma OAI.SLEExactGauge.LoewnerField.continuous_second line 126
  10. lemma OAI.SLEExactGauge.LoewnerField.first_eq line 141
  11. lemma OAI.SLEExactGauge.LoewnerField.continuous_first line 149
  12. lemma OAI.SLEExactGauge.LoewnerField.first_bound line 161
  13. lemma OAI.SLEExactGauge.LoewnerField.second_bound line 174
  14. lemma OAI.SLEExactGauge.LoewnerField.variation_of_unclipped line 186
  15. lemma OAI.SLEExactGauge.LoewnerField.drift_cancellation line 199
  16. lemma OAI.SLEExactGauge.LoewnerField.field_prefix_eq line 264
  17. def OAI.SLEExactGauge.ContinuousExit.extend line 319
  18. lemma OAI.SLEExactGauge.ContinuousExit.continuous_extend line 321
  19. lemma OAI.SLEExactGauge.ContinuousExit.extend_coe line 324
  20. def OAI.SLEExactGauge.ContinuousExit.exitSet line 327
  21. def OAI.SLEExactGauge.ContinuousExit.time line 329
  22. lemma OAI.SLEExactGauge.ContinuousExit.exitSet_nonempty line 331
  23. lemma OAI.SLEExactGauge.ContinuousExit.exitSet_subset line 333
  24. lemma OAI.SLEExactGauge.ContinuousExit.compact_exitSet line 338
  25. lemma OAI.SLEExactGauge.ContinuousExit.time_mem line 341
  26. lemma OAI.SLEExactGauge.ContinuousExit.time_bounds line 344
  27. lemma OAI.SLEExactGauge.ContinuousExit.time_le_of_nonpos line 346
  28. lemma OAI.SLEExactGauge.ContinuousExit.positive_before line 349
  29. lemma OAI.SLEExactGauge.ContinuousExit.nonpos_at_of_lt_one line 354
  30. lemma OAI.SLEExactGauge.ContinuousExit.lt_time_iff line 359
  31. lemma OAI.SLEExactGauge.ContinuousExit.isOpen_positive_on line 370
  32. lemma OAI.SLEExactGauge.ContinuousExit.measurable_time line 391
  33. lemma OAI.SLEExactGauge.ContinuousExit.time_pos line 416
  34. lemma OAI.SLEExactGauge.ContinuousExit.nonneg_until line 422
  35. lemma OAI.SLEExactGauge.ContinuousExit.eq_zero_at_of_lt_one line 432
  36. def OAI.SLEExactGauge.LoewnerExit.radius line 486
  37. def OAI.SLEExactGauge.LoewnerExit.sine line 489
  38. def OAI.SLEExactGauge.LoewnerExit.deficit line 493
  39. lemma OAI.SLEExactGauge.LoewnerExit.continuous_radius line 497
  40. lemma OAI.SLEExactGauge.LoewnerExit.continuous_sine line 502
  41. lemma OAI.SLEExactGauge.LoewnerExit.continuous_deficit line 509
  42. lemma OAI.SLEExactGauge.LoewnerExit.deficit_pos_iff line 515
  43. lemma OAI.SLEExactGauge.LoewnerExit.deficit_nonneg_iff line 520
  44. def OAI.SLEExactGauge.LoewnerExit.exitPath line 525
  45. def OAI.SLEExactGauge.LoewnerExit.stop line 533
  46. lemma OAI.SLEExactGauge.LoewnerExit.stop_bounds line 536
  47. lemma OAI.SLEExactGauge.LoewnerExit.exitPath_extend line 541
  48. lemma OAI.SLEExactGauge.LoewnerExit.exitPath_extend_div line 546
  49. lemma OAI.SLEExactGauge.LoewnerExit.positive_before line 552
  50. lemma OAI.SLEExactGauge.LoewnerExit.stop_pos line 559
  51. lemma OAI.SLEExactGauge.LoewnerExit.nonneg_until line 564
  52. lemma OAI.SLEExactGauge.LoewnerExit.nonpos_at_of_lt line 572
  53. lemma OAI.SLEExactGauge.LoewnerExit.lt_stop_iff line 581
  54. lemma OAI.SLEExactGauge.LoewnerExit.isOpen_positive_on line 600
  55. lemma OAI.SLEExactGauge.LoewnerExit.deficit_prefix_eq line 671
  56. lemma OAI.SLEExactGauge.LoewnerLocalized.regular line 729
  57. lemma OAI.SLEExactGauge.LoewnerLocalized.integral_drift_cancel line 756
  58. lemma OAI.SLEExactGauge.ContinuousDriver.aemeasurable_selectedLimit line 822
  59. lemma OAI.SLEExactGauge.ContinuousDriver.aemeasurable_path line 831
  60. def OAI.SLEExactGauge.BrownianDriver.path line 891
  61. lemma OAI.SLEExactGauge.BrownianDriver.path_measurable_past line 894
  62. lemma OAI.SLEExactGauge.BrownianDriver.path_aemeasurable line 906
  63. lemma OAI.SLEExactGauge.BrownianDriver.path_eval line 913
  64. lemma OAI.SLEExactGauge.BrownianDriver.extend_eq line 920
  65. lemma OAI.SLEExactGauge.BrownianDriver.prefix_eq line 931
  66. def OAI.SLEExactGauge.LoewnerLocalized.coeffAt line 987
  67. lemma OAI.SLEExactGauge.LoewnerLocalized.coeffAt_measurable line 993
  68. def OAI.SLEExactGauge.LoewnerLocalized.rawCoeff line 1012
  69. lemma OAI.SLEExactGauge.LoewnerLocalized.rawCoeff_measurable_past line 1016
  70. lemma OAI.SLEExactGauge.LoewnerLocalized.rawCoeff_aemeasurable line 1030
  71. lemma OAI.SLEExactGauge.LoewnerLocalized.rawCoeff_eq line 1044
  72. lemma OAI.SLEExactGauge.LoewnerLocalized.rawCoeff_stoppedCoeff_ae line 1067
  73. lemma OAI.SLEExactGauge.LoewnerLocalized.coeff_uniform_bound line 1127
  74. theorem OAI.SLEExactGauge.LoewnerLocalized.localized_centered line 1139
  75. lemma OAI.SLEExactGauge.LoewnerLocalized.field_initial line 1264
  76. theorem OAI.SLEExactGauge.LoewnerLocalized.localized_expectation line 1270
  77. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.cutoff_solution_live line 1352
  78. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivWithinAt_eval line 1387
  79. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.eq_cutoff_solution line 1408