OAI/Probability/SLEGauge/BrownianRestart.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.StoppingRounding.round line 17
  2. theorem OAI.SLEExactGauge.StoppingRounding.le_round line 19
  3. theorem OAI.SLEExactGauge.StoppingRounding.round_le line 24
  4. theorem OAI.SLEExactGauge.StoppingRounding.round_le_iff line 29
  5. theorem OAI.SLEExactGauge.StoppingRounding.floor_time_le line 36
  6. theorem OAI.SLEExactGauge.StoppingRounding.countable_range line 42
  7. theorem OAI.SLEExactGauge.StoppingRounding.tendsto_round line 47
  8. theorem OAI.SLEExactGauge.StoppingRounding.isStoppingTime line 59
  9. def OAI.SLEExactGauge.BrownianRestart.filtration line 84
  10. lemma OAI.SLEExactGauge.BrownianRestart.continuous_shift_joint line 88
  11. lemma OAI.SLEExactGauge.BrownianRestart.indep_filtration_shift line 97
  12. lemma OAI.SLEExactGauge.BrownianRestart.integral_shift line 104
  13. lemma OAI.SLEExactGauge.BrownianRestart.setIntegral_shift line 110
  14. lemma OAI.SLEExactGauge.BrownianRestart.measurable_finite_stop line 119
  15. lemma OAI.SLEExactGauge.BrownianRestart.measurable_shift_finite_stop line 128
  16. lemma OAI.SLEExactGauge.BrownianRestart.integrable_bcf_comp line 133
  17. theorem OAI.SLEExactGauge.BrownianRestart.setIntegral_shift_countable line 141
  18. theorem OAI.SLEExactGauge.BrownianRestart.setIntegral_shift_finite line 180
  19. theorem OAI.SLEExactGauge.BrownianRestart.map_shift_finite line 209
  20. theorem OAI.SLEExactGauge.BrownianRestart.indep_shift_finite line 221
  21. def OAI.SLEExactGauge.BrownianRestart.shiftAt line 249
  22. def OAI.SLEExactGauge.BrownianRestart.truncateStop line 251
  23. lemma OAI.SLEExactGauge.BrownianRestart.coe_truncateStop line 254
  24. lemma OAI.SLEExactGauge.BrownianRestart.isStoppingTime_truncateStop line 260
  25. lemma OAI.SLEExactGauge.BrownianRestart.measurable_shiftAt line 266
  26. lemma OAI.SLEExactGauge.BrownianRestart.finiteStop_iUnion_le line 271
  27. lemma OAI.SLEExactGauge.BrownianRestart.setIntegral_shiftAt_le line 281
  28. theorem OAI.SLEExactGauge.BrownianRestart.setIntegral_shiftAt_finite line 308
  29. theorem OAI.SLEExactGauge.BrownianRestart.map_shiftAt_restrict line 335
  30. theorem OAI.SLEExactGauge.BrownianRestart.map_data_shiftAt line 352
  31. theorem OAI.SLEExactGauge.BrownianRestart.lintegral_data_shiftAt line 378