OAI/Probability/SLEGauge/ReverseMoments.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.ReverseDerivative.expected_stopped_reverse_aux line 42
  2. theorem OAI.SLEExactGauge.ReverseDerivative.expected_stopped_reverseFlow line 121
  3. def OAI.SLEExactGauge.ReverseDerivative.exhaustion line 139
  4. lemma OAI.SLEExactGauge.ReverseDerivative.continuous_exhaustion line 142
  5. lemma OAI.SLEExactGauge.ReverseDerivative.exhaustion_compact line 146
  6. lemma OAI.SLEExactGauge.ReverseDerivative.exhaustion_height line 154
  7. lemma OAI.SLEExactGauge.ReverseDerivative.exhaustion_domain line 161
  8. lemma OAI.SLEExactGauge.ReverseDerivative.exhaustion_lt line 170
  9. lemma OAI.SLEExactGauge.ReverseDerivative.eventually_exhaustion_lt line 180
  10. lemma OAI.SLEExactGauge.ReverseDerivative.measurable_test line 196
  11. lemma OAI.SLEExactGauge.ReverseDerivative.test_pos line 203
  12. def OAI.SLEExactGauge.ReverseDerivative.driven line 210
  13. lemma OAI.SLEExactGauge.ReverseDerivative.measurable_driven line 213
  14. lemma OAI.SLEExactGauge.ReverseDerivative.continuousOn_driven line 220
  15. lemma OAI.SLEExactGauge.ReverseDerivative.exit_eq_horizon line 227
  16. lemma OAI.SLEExactGauge.ReverseDerivative.stopped_test_integrable line 237
  17. lemma OAI.SLEExactGauge.ReverseDerivative.lintegral_of_eventually_stopped line 267
  18. theorem OAI.SLEExactGauge.ReverseDerivative.reverse_supersolution_bound line 291
  19. lemma OAI.SLEExactGauge.ReverseDerivative.r_sub_zeta_pos line 351
  20. lemma OAI.SLEExactGauge.ReverseDerivative.exp_logderiv_le_test line 357
  21. lemma OAI.SLEExactGauge.ReverseDerivative.initial_test_scale line 384
  22. theorem OAI.SLEExactGauge.ReverseDerivative.reverse_logderiv_moment line 408
  23. abbrev OAI.SLEExactGauge.BrownianRestart.Driver line 448
  24. instance OAI.SLEExactGauge.BrownianRestart.(instance at line 449) line 449
  25. instance OAI.SLEExactGauge.BrownianRestart.(instance at line 450) line 450
  26. instance OAI.SLEExactGauge.BrownianRestart.(instance at line 451) line 451
  27. def OAI.SLEExactGauge.BrownianRestart.code line 453
  28. lemma OAI.SLEExactGauge.BrownianRestart.measurable_code line 455
  29. lemma OAI.SLEExactGauge.BrownianRestart.dense_rational_time line 458
  30. lemma OAI.SLEExactGauge.BrownianRestart.code_injective line 462
  31. lemma OAI.SLEExactGauge.BrownianRestart.code_embedding line 468