OAI/Probability/SLEGauge/TiltedMeasures.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEMain.finite_tilt_mean_one line 21
  2. def OAI.ExactSLEGreen.radialRemaining line 51
  3. def OAI.ExactSLEGreen.radialStop line 55
  4. lemma OAI.ExactSLEGreen.radialStop_actual line 61
  5. lemma OAI.ExactSLEGreen.radialStop_le_radialTime line 69
  6. lemma OAI.ExactSLEGreen.radialStop_after_survival line 79
  7. lemma OAI.ExactSLEGreen.radialStop_eventually_eq line 107
  8. lemma OAI.ExactSLEGreen.radialStop_before_tendsto line 131
  9. lemma OAI.ExactSLEGreen.radialStop_terminal_tendsto line 151
  10. lemma OAI.ExactSLEGreen.radialStop_stopping line 185
  11. lemma OAI.ExactSLEGreen.stopped_event_lt line 192
  12. lemma OAI.ExactSLEGreen.radialStop_optional line 205
  13. lemma OAI.ExactSLEGreen.radialStop_before_bound line 277
  14. lemma OAI.ExactSLEGreen.radialStop_before_measurable line 291
  15. lemma OAI.ExactSLEGreen.radialRemaining_measurable line 327
  16. theorem OAI.ExactSLEGreen.radial_conditional_weight line 340
  17. def OAI.ExactSLEGreen.stoppedRadialRemaining line 397
  18. lemma OAI.ExactSLEGreen.radialRemaining_bound line 400
  19. lemma OAI.ExactSLEGreen.radialWeight_bound line 407
  20. lemma OAI.ExactSLEGreen.radial_terminal_integrable line 415
  21. def OAI.ExactSLEGreen.capTime line 440
  22. lemma OAI.ExactSLEGreen.capTime_coe line 442
  23. lemma OAI.ExactSLEGreen.capTime_stopping line 445