OAI/Probability/SLEGauge/BrownianShifts.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.BrownianRestart.shift line 44
  2. lemma OAI.SLEExactGauge.BrownianRestart.shift_apply line 48
  3. lemma OAI.SLEExactGauge.BrownianRestart.measurable_shift line 51
  4. lemma OAI.SLEExactGauge.BrownianRestart.indep_shift_history line 56
  5. lemma OAI.SLEExactGauge.BrownianRestart.evaluation_law_unique line 70
  6. lemma OAI.SLEExactGauge.BrownianRestart.brownian_shift_map line 90
  7. lemma OAI.SLEExactGauge.BrownianRestart.shift_preserves_law line 101
  8. def OAI.SLEExactGauge.BrownianRestart.past line 110
  9. lemma OAI.SLEExactGauge.BrownianRestart.prefix_apply line 114
  10. lemma OAI.SLEExactGauge.BrownianRestart.measurable_prefix line 117
  11. def OAI.SLEExactGauge.BrownianRestart.join line 122
  12. lemma OAI.SLEExactGauge.BrownianRestart.join_apply line 134
  13. lemma OAI.SLEExactGauge.BrownianRestart.measurable_join line 137
  14. lemma OAI.SLEExactGauge.BrownianRestart.join_prefix line 148
  15. lemma OAI.SLEExactGauge.BrownianRestart.join_reconstruct line 155
  16. lemma OAI.SLEExactGauge.BrownianRestart.indep_shift_prefix line 164
  17. lemma OAI.SLEExactGauge.BrownianRestart.split_map line 181
  18. lemma OAI.SLEExactGauge.BrownianRestart.lintegral_split line 189
  19. theorem OAI.SLEExactGauge.BrownianRestart.conditional_join_kernel line 201
  20. def OAI.SLEExactGauge.BrownianRestart.reverse line 225
  21. lemma OAI.SLEExactGauge.BrownianRestart.reverse_apply line 230
  22. lemma OAI.SLEExactGauge.BrownianRestart.measurable_reverse line 233
  23. lemma OAI.SLEExactGauge.BrownianRestart.reverse_brownian line 238
  24. lemma OAI.SLEExactGauge.BrownianRestart.reverse_preserves_law line 272
  25. lemma OAI.SLEExactGauge.BrownianRestart.reverse_before line 284
  26. lemma OAI.SLEExactGauge.BrownianRestart.reverse_after line 287
  27. def OAI.SLEExactGauge.BrownianRestart.backward line 294
  28. lemma OAI.SLEExactGauge.BrownianRestart.backward_apply line 296
  29. lemma OAI.SLEExactGauge.BrownianRestart.measurable_backward line 299
  30. lemma OAI.SLEExactGauge.BrownianRestart.backward_preserves_law line 304
  31. lemma OAI.SLEExactGauge.BrownianRestart.backward_before line 316
  32. def OAI.SLEExactGauge.LiteralTrace.reversedState line 331
  33. def OAI.SLEExactGauge.LiteralTrace.reversedCurve line 335
  34. lemma OAI.SLEExactGauge.LiteralTrace.reverse_reparam_solution line 338
  35. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_eq_reversedCurve line 373
  36. lemma OAI.SLEExactGauge.ReverseDerivative.reverseFlow_log_integral line 394
  37. def OAI.SLEExactGauge.LiteralTrace.reverseCoeff line 430
  38. lemma OAI.SLEExactGauge.LiteralTrace.continuousOn_reverseCoeff line 434
  39. lemma OAI.SLEExactGauge.LiteralTrace.reversed_log_eq_integral line 451