OAI/Probability/SLEGauge/StoppedEstimates.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_local line 32
  2. structure OAI.SLEExactGauge.Parameter line 86
  3. def OAI.SLEExactGauge.Parameter.a line 93
  4. def OAI.SLEExactGauge.Parameter.d line 94
  5. def OAI.SLEExactGauge.Parameter.α line 95
  6. def OAI.SLEExactGauge.Parameter.p line 96
  7. def OAI.SLEExactGauge.Parameter.q line 98
  8. def OAI.SLEExactGauge.Parameter.η line 99
  9. def OAI.SLEExactGauge.Parameter.M line 100
  10. def OAI.SLEExactGauge.Parameter.β line 101
  11. def OAI.SLEExactGauge.Parameter.k line 102
  12. def OAI.SLEExactGauge.Parameter.A line 103
  13. def OAI.SLEExactGauge.Parameter.h₀ line 104
  14. def OAI.SLEExactGauge.Parameter.C₁ line 105
  15. def OAI.SLEExactGauge.Parameter.c₁ line 106
  16. def OAI.SLEExactGauge.Parameter.δ line 108
  17. def OAI.SLEExactGauge.Parameter.f line 110
  18. def OAI.SLEExactGauge.Parameter.D line 111
  19. def OAI.SLEExactGauge.Parameter.drift line 113
  20. lemma OAI.SLEExactGauge.Parameter.a_gt_quarter line 117
  21. lemma OAI.SLEExactGauge.Parameter.p_pos line 122
  22. lemma OAI.SLEExactGauge.Parameter.q_pos line 126
  23. lemma OAI.SLEExactGauge.Parameter.q_le_half line 130
  24. lemma OAI.SLEExactGauge.Parameter.q_lt_one line 134
  25. lemma OAI.SLEExactGauge.Parameter.q_lt_p line 137
  26. lemma OAI.SLEExactGauge.Parameter.k_pos line 141
  27. lemma OAI.SLEExactGauge.Parameter.A_pos line 145
  28. lemma OAI.SLEExactGauge.Parameter.β_le_one line 150
  29. lemma OAI.SLEExactGauge.Parameter.h₀_pos line 152
  30. lemma OAI.SLEExactGauge.Parameter.h₀_lt_one line 156
  31. lemma OAI.SLEExactGauge.Parameter.h₀_power line 166
  32. lemma OAI.SLEExactGauge.Parameter.f_pos line 177
  33. def OAI.SLEExactGauge.Parameter.RegularizedDriftObligation line 183
  34. theorem OAI.SLEExactGauge.Parameter.regularized_drift_bound line 188
  35. lemma OAI.SLEExactGauge.Parameter.η_pos line 256
  36. lemma OAI.SLEExactGauge.Parameter.η_lt_half line 260
  37. lemma OAI.SLEExactGauge.Parameter.η_exponent line 265
  38. lemma OAI.SLEExactGauge.Parameter.M_pos line 271
  39. lemma OAI.SLEExactGauge.Parameter.M_formula line 275
  40. lemma OAI.SLEExactGauge.Parameter.β_pos line 285
  41. lemma OAI.SLEExactGauge.Parameter.interaction_exponent_lt line 291
  42. lemma OAI.SLEExactGauge.Parameter.f_ge_δ line 298
  43. lemma OAI.SLEExactGauge.Parameter.f_le_three line 305
  44. def OAI.SLEExactGauge.Parameter.angularDerivative line 314
  45. lemma OAI.SLEExactGauge.Parameter.angularDerivative_bound line 317
  46. theorem OAI.SLEExactGauge.Parameter.normalized_angularDerivative_bound line 339
  47. def OAI.SLEExactGauge.Parameter.angleGenerator line 384
  48. lemma OAI.SLEExactGauge.Parameter.hasDerivAt_sinePower line 387
  49. lemma OAI.SLEExactGauge.Parameter.hasDerivAt_sinePower_first line 393
  50. lemma OAI.SLEExactGauge.Parameter.deriv_sinePower line 406
  51. lemma OAI.SLEExactGauge.Parameter.secondDeriv_sinePower line 410
  52. theorem OAI.SLEExactGauge.Parameter.sine_generator line 420
  53. lemma OAI.SLEExactGauge.Parameter.hasDerivAt_factor line 434
  54. def OAI.SLEExactGauge.Parameter.C₂ line 443
  55. def OAI.SLEExactGauge.Parameter.youngConstant line 446
  56. lemma OAI.SLEExactGauge.Parameter.C₂_pos line 450