OAI/Probability/SLEGauge/OptionalGreen.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGreen.stoppedSurvivingGreen line 21
  2. def OAI.ExactSLEGreen.stoppedRemainingDensity line 26
  3. lemma OAI.ExactSLEGreen.stoppedSurvivingGreen_nonneg line 30
  4. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_nonneg line 38
  5. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_le_surviving line 46
  6. lemma OAI.ExactSLEGreen.stopped_remaining_to_surviving line 54
  7. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_eq line 66
  8. lemma OAI.ExactSLEGreen.stoppedRadialTerminal_integrable line 73
  9. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_mean_bound line 89
  10. theorem OAI.ExactSLEGreen.survivingGreen_optional_bound line 116
  11. lemma OAI.ExactSLEGreen.stopped_remaining_integral_tendsto line 157
  12. theorem OAI.ExactSLEGreen.survivingGreen_optional_comparison line 181
  13. lemma OAI.ExactSLEGreen.radialRemaining_time_joint_measurable line 240
  14. lemma OAI.ExactSLEGenerator.pastDriver_stopping_measurable line 303
  15. lemma OAI.ExactSLEGreen.remainingMassDensity_time_joint_measurable line 350
  16. lemma OAI.ExactSLEGreen.survivingGreen_time_joint_measurable line 360
  17. lemma OAI.ExactSLEGreen.survivingGreen_driver_congr line 375
  18. theorem OAI.ExactSLEGreen.stoppedSurvivingGreen_raw_joint line 382
  19. lemma OAI.ExactSLEGreen.stoppedSurvivingGreen_joint_measurable line 411
  20. theorem OAI.ExactSLEGreen.stoppedRemainingDensity_raw_joint line 420
  21. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_joint_measurable line 453
  22. lemma OAI.ExactSLEGreen.localState_fst_eq_solution line 476
  23. lemma OAI.ExactSLEGreen.localState_eq_actual_of_height line 502
  24. lemma OAI.ExactSLEGreen.localState_eventually_eq_actual line 519
  25. lemma OAI.ExactSLEGreen.survivingGreen_pos_iff line 529
  26. lemma OAI.ExactSLEGreen.measurableSet_alive_joint line 537
  27. def OAI.ExactSLEGreen.killedState line 544
  28. lemma OAI.ExactSLEGreen.killedState_time_joint_measurable line 547
  29. lemma OAI.ExactSLEGreen.loewnerMap_time_joint_measurable line 567