OAI/Probability/SLELocalization/ReverseFlow.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Reverse Loewner estimates.

  1. lemma OAI.SLEExactGauge.ReverseLoewner.continuous_velocity line 17
  2. lemma OAI.SLEExactGauge.ReverseLoewner.norm_velocity_le line 21
  3. lemma OAI.SLEExactGauge.ReverseLoewner.exists_solution line 25
  4. lemma OAI.SLEExactGauge.ReverseLoewner.norm_velocity_driver_sub_le line 60
  5. lemma OAI.SLEExactGauge.ReverseLoewner.derivWithin_right line 65
  6. lemma OAI.SLEExactGauge.ReverseLoewner.derivWithin_left line 71
  7. lemma OAI.SLEExactGauge.ReverseLoewner.solution_eq line 77
  8. lemma OAI.SLEExactGauge.ReverseLoewner.solution_dist_le line 87
  9. def OAI.SLEExactGauge.ReverseLoewner.solution line 137
  10. lemma OAI.SLEExactGauge.ReverseLoewner.solution_initial line 140
  11. lemma OAI.SLEExactGauge.ReverseLoewner.solution_deriv line 145
  12. def OAI.SLEExactGauge.ReverseLoewner.solutionPath line 151
  13. lemma OAI.SLEExactGauge.ReverseLoewner.solutionPath_lipschitz line 156
  14. def OAI.SLEExactGauge.ReverseLoewner.reverseCentered line 188
  15. lemma OAI.SLEExactGauge.ReverseLoewner.reverseCentered_lipschitz line 192
  16. lemma OAI.SLEExactGauge.ReverseLoewner.extend_reverseCentered line 203
  17. lemma OAI.SLEExactGauge.ReverseLoewner.extend_end line 210
  18. def OAI.SLEExactGauge.ReverseLoewner.tipApprox line 215
  19. lemma OAI.SLEExactGauge.ReverseLoewner.continuous_tipApprox line 218
  20. lemma OAI.SLEExactGauge.ReverseLoewner.tipApprox_eq_inverse line 226
  21. def OAI.SLEExactGauge.CanonicalTrace.height line 279
  22. lemma OAI.SLEExactGauge.CanonicalTrace.height_pos line 281
  23. lemma OAI.SLEExactGauge.CanonicalTrace.height_tendsto line 283
  24. def OAI.SLEExactGauge.CanonicalTrace.value line 291
  25. lemma OAI.SLEExactGauge.CanonicalTrace.measurable_past line 295
  26. lemma OAI.SLEExactGauge.CanonicalTrace.aemeasurable line 311
  27. lemma OAI.SLEExactGauge.CanonicalTrace.eq_source line 326
  28. theorem OAI.SLEExactGauge.canonicalTraceFromBrownianPast line 358
  29. lemma OAI.SLEExactGauge.BoundaryGreen.source_point_reach line 387
  30. lemma OAI.SLEExactGauge.BoundaryGreen.source_hit_eventually_reach line 411
  31. lemma OAI.SLEExactGauge.BoundaryGreen.initial_bound line 452
  32. def OAI.SLEExactGauge.BoundaryGreen.uniformBudget line 464
  33. lemma OAI.SLEExactGauge.BoundaryGreen.uniformBudget_mean line 468
  34. lemma OAI.SLEExactGauge.BoundaryGreen.uniformBudget_dominates line 486
  35. lemma OAI.SLEExactGauge.BoundaryGreen.ratio_power_eq line 491
  36. theorem OAI.SLEExactGauge.BoundaryGreen.positive_real_bound line 497
  37. def OAI.SLEExactGauge.BoundaryGreen.mirror line 540
  38. lemma OAI.SLEExactGauge.BoundaryGreen.mirror_im line 542
  39. lemma OAI.SLEExactGauge.BoundaryGreen.mirror_re line 544
  40. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_mirror line 546
  41. lemma OAI.SLEExactGauge.BoundaryGreen.mirror_dist_real line 548
  42. lemma OAI.SLEExactGauge.BoundaryGreen.mirror_ode line 553
  43. lemma OAI.SLEExactGauge.BoundaryGreen.negative_source_point_reach line 561
  44. lemma OAI.SLEExactGauge.BoundaryGreen.negative_source_hit_eventually_reach line 587
  45. theorem OAI.SLEExactGauge.BoundaryGreen.negative_real_bound line 633
  46. theorem OAI.SLEExactGauge.BoundaryGreen.real_bound line 675
  47. lemma OAI.SLEExactGauge.BoundaryGreen.annulus_real_bound line 689
  48. def OAI.SLEExactGauge.AngularBarrier.lowerGamma line 720
  49. def OAI.SLEExactGauge.AngularBarrier.cdf line 722
  50. def OAI.SLEExactGauge.AngularBarrier.pdf line 724
  51. lemma OAI.SLEExactGauge.AngularBarrier.integrable_kernel line 726
  52. lemma OAI.SLEExactGauge.AngularBarrier.kernel_continuousAt line 731
  53. lemma OAI.SLEExactGauge.AngularBarrier.lowerGamma_nonneg line 736
  54. lemma OAI.SLEExactGauge.AngularBarrier.cdf_nonneg line 741
  55. lemma OAI.SLEExactGauge.AngularBarrier.pdf_pos line 744
  56. lemma OAI.SLEExactGauge.AngularBarrier.power_integral line 747
  57. lemma OAI.SLEExactGauge.AngularBarrier.cdf_le_power line 752
  58. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_lowerGamma line 764
  59. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_cdf line 771
  60. lemma OAI.SLEExactGauge.AngularBarrier.deriv_cdf line 775
  61. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_pdf line 778
  62. lemma OAI.SLEExactGauge.AngularBarrier.lowerGamma_tendsto line 789
  63. lemma OAI.SLEExactGauge.AngularBarrier.cdf_tendsto line 794
  64. lemma OAI.SLEExactGauge.AngularBarrier.power_mul line 800
  65. lemma OAI.SLEExactGauge.AngularBarrier.kernel_lower line 806
  66. lemma OAI.SLEExactGauge.AngularBarrier.lowerGamma_lower line 818
  67. lemma OAI.SLEExactGauge.AngularBarrier.cdf_pdf_inequality line 835
  68. lemma OAI.SLEExactGauge.AngularBarrier.contDiffAt_pdf line 849
  69. lemma OAI.SLEExactGauge.AngularBarrier.contDiffOn_cdf line 857
  70. lemma OAI.SLEExactGauge.AngularBarrier.contDiffAt_cdf line 867
  71. def OAI.SLEExactGauge.AngularBarrier.scale line 872
  72. def OAI.SLEExactGauge.AngularBarrier.value line 874
  73. def OAI.SLEExactGauge.AngularBarrier.valueQ line 876
  74. def OAI.SLEExactGauge.AngularBarrier.valueQQ line 878
  75. def OAI.SLEExactGauge.AngularBarrier.valueT line 881
  76. lemma OAI.SLEExactGauge.AngularBarrier.scale_pos line 885
  77. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_scale line 891
  78. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_value_q line 897
  79. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_valueQ_q line 906
  80. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_value_t line 915
  81. theorem OAI.SLEExactGauge.AngularBarrier.supersolution line 930
  82. lemma OAI.SLEExactGauge.AngularBarrier.value_nonneg line 967
  83. lemma OAI.SLEExactGauge.AngularBarrier.contDiffAt_value line 971
  84. lemma OAI.SLEExactGauge.AngularBarrier.continuousAt_value line 984
  85. lemma OAI.SLEExactGauge.AngularBarrier.scale_tendsto line 989
  86. lemma OAI.SLEExactGauge.AngularBarrier.value_tendsto_zero_time line 998