OAI/Probability/SLEGauge/RawBrownianRestart.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.LoewnerRestart.restart line 21
  2. lemma OAI.SLEExactGauge.LoewnerRestart.restart_apply line 24
  3. lemma OAI.SLEExactGauge.LoewnerRestart.continuous_restart_joint line 27
  4. def OAI.SLEExactGauge.LoewnerRestart.restartAt line 32
  5. lemma OAI.SLEExactGauge.LoewnerRestart.comap_rawFiltration line 34
  6. lemma OAI.SLEExactGauge.LoewnerRestart.measurable_driver_raw line 40
  7. lemma OAI.SLEExactGauge.LoewnerRestart.measurable_driver_raw_all line 44
  8. lemma OAI.SLEExactGauge.LoewnerRestart.stoppingTime_transport line 49
  9. lemma OAI.SLEExactGauge.LoewnerRestart.measurable_driver_stopped line 54
  10. lemma OAI.SLEExactGauge.LoewnerRestart.measurable_restartAt line 61
  11. lemma OAI.SLEExactGauge.LoewnerRestart.restartAt_transport line 66
  12. lemma OAI.SLEExactGauge.LoewnerRestart.setIntegral_restartAt line 72
  13. theorem OAI.SLEExactGauge.LoewnerRestart.map_restartAt_restrict line 100
  14. theorem OAI.SLEExactGauge.LoewnerRestart.map_data_restartAt line 116
  15. theorem OAI.SLEExactGauge.LoewnerRestart.lintegral_data_restartAt line 139
  16. lemma OAI.ExactSLEGreen.actualState_restart line 166
  17. lemma OAI.ExactSLEGreen.physicalRadius_add_log line 182
  18. lemma OAI.ExactSLEGreen.logGreen_add_log line 187
  19. lemma OAI.ExactSLEGreen.physicalGreen_add_log line 192
  20. lemma OAI.ExactSLEGreen.physicalRadius_restart line 198
  21. lemma OAI.ExactSLEGreen.physicalGreen_restart line 210
  22. lemma OAI.SLEExactGauge.LoewnerRestart.restart_eq_shiftDriver line 227
  23. theorem OAI.SLEExactGauge.LoewnerRestart.survivingGreen_restart line 232
  24. theorem OAI.SLEExactGauge.LoewnerRestart.survivingGreen_restart_ratio line 249
  25. lemma OAI.ExactSLECalculus.N_rpow line 275
  26. lemma OAI.ExactSLECalculus.L_rpow line 282
  27. def OAI.ExactSLEGreen.centeredGenerator line 302
  28. lemma OAI.ExactSLEGreen.green_product_generator line 305
  29. lemma OAI.ExactSLEGreen.N_Q line 319
  30. lemma OAI.ExactSLEGreen.L_Q line 323
  31. lemma OAI.ExactSLEGreen.N_Y line 334
  32. lemma OAI.ExactSLEGreen.L_Y line 338
  33. lemma OAI.ExactSLEGreen.centeredGenerator_Qpow line 345
  34. lemma OAI.ExactSLEGreen.centeredGenerator_Ypow line 362
  35. def OAI.ExactSLEGreen.lifetimeTest line 375
  36. lemma OAI.ExactSLEGreen.lifetimeTest_smooth line 378
  37. lemma OAI.ExactSLEGreen.lifetimeTest_nonneg line 383
  38. lemma OAI.ExactSLEGreen.lifetimeTest_coercive line 388
  39. lemma OAI.ExactSLEGreen.centeredGenerator_lifetimeTest line 393
  40. lemma OAI.ExactSLEGreen.height_power_comparison line 412
  41. lemma OAI.ExactSLEGreen.centeredGenerator_lifetimeTest_le line 426
  42. def OAI.ExactSLEGreen.lifetimeExponent line 449
  43. def OAI.ExactSLEGreen.lifetimeDrift line 450
  44. lemma OAI.ExactSLEGreen.lifetimeExponent_pos line 453
  45. lemma OAI.ExactSLEGreen.lifetimeExponent_le_one line 457
  46. lemma OAI.ExactSLEGreen.lifetimeDrift_pos line 459
  47. lemma OAI.ExactSLEGreen.green_lifetime_generator_le line 465