OAI/Probability/SLEGauge/AngleGenerators.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.physicalTheta_second_noise line 20
  2. lemma OAI.ExactSLEGreen.regX_drift line 40
  3. lemma OAI.ExactSLEGreen.regY_drift line 42
  4. lemma OAI.ExactSLEGreen.regJ_drift line 44
  5. lemma OAI.ExactSLEGreen.theta_generator line 50
  6. def OAI.ExactSLEGreen.physicalClock line 62
  7. def OAI.ExactSLEGreen.clockDeriv line 64
  8. lemma OAI.ExactSLEGreen.hasFDerivAt_physicalClock line 66
  9. lemma OAI.ExactSLEGreen.clockDeriv_noise line 73
  10. lemma OAI.ExactSLEGreen.physicalClock_drift line 75
  11. lemma OAI.ExactSLEGreen.physicalClock_second_noise line 85
  12. lemma OAI.ExactSLEGreen.physicalTheta_smooth line 92
  13. lemma OAI.ExactSLEGreen.physicalClock_smooth line 94
  14. def OAI.ExactSLECalculus.N line 104
  15. def OAI.ExactSLECalculus.L line 105
  16. lemma OAI.ExactSLECalculus.N_differentiableAt line 107
  17. lemma OAI.ExactSLECalculus.N_mul line 110
  18. lemma OAI.ExactSLECalculus.L_mul line 116
  19. lemma OAI.ExactSLECalculus.N_comp line 134
  20. lemma OAI.ExactSLECalculus.L_comp line 139
  21. lemma OAI.ExactSLECalculus.N_const line 165
  22. lemma OAI.ExactSLECalculus.L_const line 167
  23. lemma OAI.ExactSLECalculus.N_add line 171
  24. lemma OAI.ExactSLECalculus.L_add line 177
  25. lemma OAI.ExactSLECalculus.N_const_mul line 193
  26. lemma OAI.ExactSLECalculus.L_const_mul line 196
  27. def OAI.ExactSLEFiniteTilt.sinePower line 205
  28. def OAI.ExactSLEFiniteTilt.angleGenerator line 206
  29. theorem OAI.ExactSLEFiniteTilt.sinePower_hasDerivAt line 212
  30. theorem OAI.ExactSLEFiniteTilt.sinePower_secondDeriv line 216
  31. theorem OAI.ExactSLEFiniteTilt.angleGenerator_sinePower line 233
  32. theorem OAI.ExactSLEFiniteTilt.sine_generator line 245
  33. theorem OAI.ExactSLEFiniteTilt.green_angle_eigenfunction line 254
  34. theorem OAI.ExactSLEFiniteTilt.tilted_lyapunov line 260
  35. def OAI.ExactSLEGreen.clockExp line 280
  36. def OAI.ExactSLEGreen.angleLift line 282
  37. lemma OAI.ExactSLEGreen.clock_N_zero line 283
  38. lemma OAI.ExactSLEGreen.clock_L line 286
  39. lemma OAI.ExactSLEGreen.theta_N line 292
  40. lemma OAI.ExactSLEGreen.theta_L line 294
  41. lemma OAI.ExactSLEGreen.clockExp_smooth line 297
  42. lemma OAI.ExactSLEGreen.clockExp_N line 300
  43. lemma OAI.ExactSLEGreen.clockExp_L line 307
  44. lemma OAI.ExactSLEGreen.angleLift_smooth line 317
  45. lemma OAI.ExactSLEGreen.angleLift_N line 320
  46. lemma OAI.ExactSLEGreen.angleLift_L line 325
  47. lemma OAI.ExactSLEGreen.exponential_angle_generator line 333
  48. lemma OAI.ExactSLEGreen.sinePower_smooth line 341
  49. def OAI.ExactSLEFiniteTilt.regP line 346
  50. def OAI.ExactSLEFiniteTilt.regQ line 347
  51. def OAI.ExactSLEFiniteTilt.regEta line 348
  52. def OAI.ExactSLEFiniteTilt.regM line 349
  53. def OAI.ExactSLEFiniteTilt.regBeta line 350
  54. def OAI.ExactSLEFiniteTilt.regK line 351
  55. def OAI.ExactSLEFiniteTilt.regA line 352
  56. def OAI.ExactSLEFiniteTilt.regH line 353
  57. def OAI.ExactSLEFiniteTilt.regC line 354
  58. def OAI.ExactSLEFiniteTilt.regFactor line 355
  59. def OAI.ExactSLEFiniteTilt.regD line 357
  60. def OAI.ExactSLEFiniteTilt.regNormalizedDrift line 358
  61. lemma OAI.ExactSLEFiniteTilt.regP_pos line 365
  62. lemma OAI.ExactSLEFiniteTilt.regQ_pos line 366
  63. lemma OAI.ExactSLEFiniteTilt.regQ_lt_one line 368
  64. lemma OAI.ExactSLEFiniteTilt.regQ_lt_p line 371
  65. lemma OAI.ExactSLEFiniteTilt.regEta_pos line 375
  66. lemma OAI.ExactSLEFiniteTilt.regEta_lt_half line 378
  67. lemma OAI.ExactSLEFiniteTilt.regEta_identity line 384
  68. lemma OAI.ExactSLEFiniteTilt.regM_pos line 389
  69. lemma OAI.ExactSLEFiniteTilt.regM_eq line 393
  70. lemma OAI.ExactSLEFiniteTilt.regBeta_pos line 402
  71. lemma OAI.ExactSLEFiniteTilt.regBeta_le_one line 404
  72. lemma OAI.ExactSLEFiniteTilt.regBeta_discount line 405
  73. lemma OAI.ExactSLEFiniteTilt.regK_pos line 411
  74. lemma OAI.ExactSLEFiniteTilt.regA_pos line 413
  75. lemma OAI.ExactSLEFiniteTilt.reg_base_lt_one line 418
  76. lemma OAI.ExactSLEFiniteTilt.regH_pos line 427
  77. lemma OAI.ExactSLEFiniteTilt.regH_lt_one line 429
  78. lemma OAI.ExactSLEFiniteTilt.regH_power line 433
  79. lemma OAI.ExactSLEFiniteTilt.regC_pos line 441