OAI/Probability/SLEGauge/RandomRestrictionKernel.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.MassVersions.measurable_random_restrict line 16
  2. lemma OAI.SLEExactGauge.TraceRestriction.tendsto_integral_visited_atTop line 49
  3. lemma OAI.SLEExactGauge.TraceRestriction.continuous_integral_restrict_visited line 65
  4. lemma OAI.SLEExactGauge.TraceRestriction.tendsto_integral_restrict_visited_atTop line 73
  5. lemma OAI.SLEExactGauge.LoewnerRestart.measurableSet_alive_atStop_raw line 98
  6. lemma OAI.SLEExactGauge.LoewnerRestart.measurableSet_alive_spatial line 115
  7. def OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop line 120
  8. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_raw_measurable line 126
  9. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_terminal_measurable line 141
  10. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_measurable line 158
  11. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_finiteOnCompacts line 168
  12. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_compact_stronglyAdapted line 178
  13. theorem OAI.SLEExactGauge.MassVersions.ae_finiteOnCompacts_of_average line 206
  14. lemma OAI.SLEExactGauge.MassVersions.compact_eval_integrable_of_average line 221
  15. lemma OAI.SLEExactGauge.MassVersions.ae_compact_integrable_of_average line 229
  16. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_terminal_le line 252
  17. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_terminal_integrable line 262
  18. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_zero_of_convergence line 281
  19. theorem OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_path_properties line 301
  20. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_integral line 371
  21. lemma OAI.SLEExactGauge.LoewnerRestart.integrable_restartPush_iff line 381
  22. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_mono line 392
  23. lemma OAI.SLEExactGauge.LoewnerRestart.ae_restartAt line 401
  24. theorem OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_terminal_regular line 416
  25. lemma OAI.SLEExactGauge.LoewnerRestart.continuous_restartPush_visited line 451
  26. lemma OAI.SLEExactGauge.LoewnerRestart.tendsto_restartPush_visited_atTop line 461
  27. theorem OAI.SLEExactGauge.LoewnerRestart.recoveredRestart_path_properties line 474
  28. lemma OAI.SLEExactGauge.MassVersions.random_restrict_test_lintegral line 552
  29. lemma OAI.SLEExactGauge.MassVersions.conditional_random_restrict_on line 565