OAI/Probability/SLEGauge/StoppedMassMeasurability.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGenerator.stoppedPastDriver line 19
  2. lemma OAI.ExactSLEGenerator.stoppedPastDriver_apply line 22
  3. lemma OAI.ExactSLEGenerator.stoppedPastDriver_measurable line 33
  4. lemma OAI.ExactSLEGreen.timeMassDensity_stoppedPastDriver line 65
  5. theorem OAI.ExactSLEGreen.timeMassDensity_stopping_raw_joint line 80
  6. lemma OAI.ExactSLEGreen.actualUpperMass_stopping_raw_measurable line 102
  7. lemma OAI.ExactSLEGreen.actualUpperMass_stopping_eval_raw_measurable line 116
  8. lemma OAI.ExactSLEGreen.actualUpperMass_stopping_eval_measurable line 129
  9. theorem OAI.ExactSLEGreen.recoveredMass_stopping_raw_measurable line 139
  10. lemma OAI.ExactSLEGreen.recoveredMass_stopping_measurable line 151
  11. lemma OAI.ExactSLEGreen.actual_stopped_radon_limit_memLp line 172
  12. lemma OAI.ExactSLEGreen.actual_stopped_radon_limit_L1 line 210
  13. lemma OAI.ExactSLEGreen.actual_stopped_radon_mass_extraction line 256
  14. theorem OAI.ExactSLEGreen.actual_raw_stopped_extraction line 307
  15. lemma OAI.ExactSLEGreen.actual_stopped_limit_compact_conditional line 379
  16. theorem OAI.ExactSLEGreen.stopped_compact_conditional_to_random_tests line 434
  17. theorem OAI.ExactSLEGreen.stopped_conditional_future_support line 498