OAI/Probability/SLELocalization/TraceModel.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Boundary Cutoff estimates.

  1. lemma OAI.SLEExactGauge.BoundaryCutoff.norm_velocity_sub_le line 16
  2. lemma OAI.SLEExactGauge.BoundaryCutoff.velocity_lipschitz line 38
  3. lemma OAI.SLEExactGauge.BoundaryCutoff.continuous_velocity line 45
  4. lemma OAI.SLEExactGauge.BoundaryCutoff.exists_solution line 54
  5. lemma OAI.SLEExactGauge.BoundaryCutoff.norm_velocity_driver_sub_le line 74
  6. lemma OAI.SLEExactGauge.BoundaryCutoff.derivWithin_right line 83
  7. lemma OAI.SLEExactGauge.BoundaryCutoff.derivWithin_left line 89
  8. lemma OAI.SLEExactGauge.BoundaryCutoff.clamp_conj line 95
  9. lemma OAI.SLEExactGauge.BoundaryCutoff.velocity_conj line 99
  10. lemma OAI.SLEExactGauge.BoundaryCutoff.conjugate_deriv line 104
  11. lemma OAI.SLEExactGauge.BoundaryCutoff.positive_height line 113
  12. lemma OAI.SLEExactGauge.BoundaryCutoff.solution_dist_le line 140
  13. structure OAI.SLEExactGauge.Gauge line 188
  14. instance OAI.SLEExactGauge.(instance at line 195) line 195
  15. def OAI.SLEExactGauge.Gauge.extended line 197
  16. def OAI.SLEExactGauge.Gauge.hausdorff line 200
  17. def OAI.SLEExactGauge.IsExactGauge line 203
  18. def OAI.SLEExactGauge.IsLargerGauge line 208
  19. def OAI.SLEExactGauge.halfPlane line 212
  20. def OAI.SLEExactGauge.localizationSegment line 214
  21. def OAI.SLEExactGauge.localizationWholeTrace line 216
  22. def OAI.SLEExactGauge.rectangle line 218
  23. def OAI.SLEExactGauge.localizationDomain line 221
  24. def OAI.SLEExactGauge.IsLoewnerTrace line 225
  25. def OAI.SLEExactGauge.IsChordalSLE line 245
  26. def OAI.SLEExactGauge.LocalizationMainEvent line 251
  27. def OAI.SLEExactGauge.LocalizationMainConclusion line 256
  28. def OAI.SLEExactGauge.LargerGaugeConclusion line 262
  29. def OAI.SLEExactGauge.IsLoewnerTraceUsing line 267
  30. def OAI.SLEExactGauge.loewnerRadius line 287
  31. def OAI.SLEExactGauge.loewnerAngleSine line 290
  32. def OAI.SLEExactGauge.firstLiveRadiusStop line 294
  33. def OAI.SLEExactGauge.finiteStoppedDensity line 300
  34. lemma OAI.SLEExactGauge.halfPlane_open line 307
  35. lemma OAI.SLEExactGauge.halfPlane_preconnected line 310
  36. lemma OAI.SLEExactGauge.halfPlane_not_bounded line 313
  37. lemma OAI.SLEExactGauge.survivingDomain_mono line 323
  38. lemma OAI.SLEExactGauge.survivingDomain_zero line 331
  39. lemma OAI.SLEExactGauge.survivingDomain_open line 347
  40. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.initial line 376
  41. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_eval line 379
  42. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.im_pos line 387
  43. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.analytic_eval line 391
  44. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.deriv_initial line 395
  45. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivAt_eval line 403
  46. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.deriv_ne_zero line 409
  47. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_pos line 423
  48. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_initial line 430
  49. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.centered_ne_zero line 434
  50. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivAt_height line 443
  51. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.height_antitone line 450
  52. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.height_le_initial line 466
  53. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_velocity line 472
  54. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.integral_velocity line 481
  55. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.norm_velocity_le line 495
  56. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.norm_time_sub_le line 508
  57. lemma OAI.SLEExactGauge.firstLiveRadiusStop_zero line 535
  58. def OAI.SLEExactGauge.IsLoewnerTraceUsing.differenceCoefficient line 557
  59. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_differenceCoefficient line 560
  60. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.difference_eq_exp_integral line 571
  61. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuousAt_integral_differenceCoefficient line 616
  62. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.spatial_deriv_eq_exp_integral line 658
  63. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.log_deriv_norm_eq line 682
  64. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_spatialCoefficient line 689
  65. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_log_deriv_norm line 697
  66. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivAt_log_deriv_norm line 711
  67. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.real_spatialCoefficient line 731
  68. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.log_radius_eq line 738
  69. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_log_radius line 746
  70. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivAt_log_radius line 756
  71. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.continuous_radius line 779
  72. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.log_radius_strictAnti line 787
  73. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_strictAnti line 805
  74. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.live_radius_injective line 814
  75. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.firstLiveRadiusStop_eq line 825