OAI/Probability/SLEGauge/RawRestartTests.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.LoewnerRestart.map_data_restartAt_on line 18
  2. theorem OAI.SLEExactGauge.LoewnerRestart.lintegral_data_restartAt_on line 45
  3. lemma OAI.SLEExactGauge.LoewnerRestart.kernel_with_data_measurable line 74
  4. lemma OAI.SLEExactGauge.LoewnerRestart.lintegral_kernel_restartAt_on_shift line 83
  5. theorem OAI.SLEExactGauge.LoewnerRestart.restartAt_conditional_kernel line 113
  6. lemma OAI.SLEExactGauge.LoewnerRestart.survivingGreen_zero line 174
  7. lemma OAI.SLEExactGauge.LoewnerRestart.survivingKernel_zero line 180
  8. lemma OAI.SLEExactGauge.LoewnerRestart.survivingKernel_restrict_alive line 185
  9. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_initialGreen line 198
  10. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_test_joint_measurable line 206
  11. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_mean line 218
  12. theorem OAI.SLEExactGauge.LoewnerRestart.restartPush_stopped_terminal_mean line 235
  13. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_measure_joint_measurable line 265
  14. def OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel line 277
  15. lemma OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_apply line 292
  16. theorem OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_average_on line 300
  17. theorem OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_average_le_initial line 333
  18. theorem OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_compact_lintegral_lt_top line 347
  19. lemma OAI.SLEExactGauge.LoewnerRestart.restartPullback_joint_measurable line 373
  20. theorem OAI.SLEExactGauge.LoewnerRestart.restartPush_conditional_kernel line 390
  21. theorem OAI.SLEExactGauge.LoewnerRestart.recoveredMass_restarted_potential line 425
  22. def OAI.SLEExactGauge.LoewnerRestart.afterStopFiltration line 487
  23. lemma OAI.SLEExactGauge.LoewnerRestart.raw_function_congr line 496
  24. lemma OAI.SLEExactGauge.LoewnerRestart.raw_measure_congr line 503
  25. def OAI.SLEExactGauge.LoewnerRestart.freshPast line 511
  26. lemma OAI.SLEExactGauge.LoewnerRestart.freshPast_raw_measurable line 515
  27. lemma OAI.SLEExactGauge.LoewnerRestart.freshPast_eq line 525
  28. lemma OAI.SLEExactGauge.LoewnerRestart.restartCandidateKernel_raw_measurable line 539
  29. def OAI.SLEExactGauge.LoewnerRestart.recoveredRestart line 567
  30. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredRestart_measurable line 573
  31. lemma OAI.SLEExactGauge.LoewnerRestart.recoveredRestart_compact_stronglyAdapted line 583