OAI/Probability/SLEGauge/LoewnerScaling.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.LoewnerScaling.scaled line 21
  2. lemma OAI.SLEExactGauge.LoewnerScaling.scaled_scaled line 24
  3. lemma OAI.SLEExactGauge.LoewnerScaling.scaled_continuous line 31
  4. def OAI.SLEExactGauge.LoewnerScaling.scaleDriver line 35
  5. lemma OAI.SLEExactGauge.LoewnerScaling.scaleDriver_apply line 38
  6. lemma OAI.SLEExactGauge.LoewnerScaling.scaleDriver_inv line 41
  7. lemma OAI.SLEExactGauge.LoewnerScaling.continuous_scaleDriver line 47
  8. lemma OAI.SLEExactGauge.LoewnerScaling.odeUntil_scaled line 55
  9. lemma OAI.SLEExactGauge.LoewnerScaling.alive_scaled_iff line 86
  10. lemma OAI.SLEExactGauge.LoewnerScaling.loewnerMap_scaled line 104
  11. lemma OAI.SLEExactGauge.LoewnerScaling.deriv_loewnerMap_scaled line 115
  12. lemma OAI.SLEExactGauge.LoewnerScaling.actualState_scaled line 133
  13. abbrev OAI.SLEExactGauge.FlowIdentification.TDriver line 158
  14. abbrev OAI.SLEExactGauge.FlowIdentification.GDriver line 159
  15. def OAI.SLEExactGauge.FlowIdentification.driverHomeomorph line 162
  16. lemma OAI.SLEExactGauge.FlowIdentification.driverHomeomorph_apply line 171
  17. lemma OAI.SLEExactGauge.FlowIdentification.driverHomeomorph_symm_apply line 174
  18. lemma OAI.SLEExactGauge.FlowIdentification.measurable_driverHomeomorph line 177
  19. lemma OAI.SLEExactGauge.FlowIdentification.measurable_driverHomeomorph_symm line 180
  20. def OAI.SLEExactGauge.FlowIdentification.driverMeasurableEquiv line 183
  21. lemma OAI.SLEExactGauge.FlowIdentification.brownian_map_driver line 186
  22. lemma OAI.SLEExactGauge.FlowIdentification.positiveSolution_iff line 197
  23. lemma OAI.SLEExactGauge.FlowIdentification.eulerSteps_eq line 207
  24. lemma OAI.SLEExactGauge.FlowIdentification.eulerFlow_eq line 215
  25. lemma OAI.SLEExactGauge.FlowIdentification.cutoffFlow_eq line 220
  26. lemma OAI.SLEExactGauge.FlowIdentification.surviving_eq line 224
  27. lemma OAI.SLEExactGauge.FlowIdentification.surviving_iff_alive line 228
  28. lemma OAI.SLEExactGauge.FlowIdentification.flow_eq_literal line 233
  29. lemma OAI.SLEExactGauge.FlowIdentification.flow_eq_loewnerMap line 249
  30. lemma OAI.SLEExactGauge.FlowIdentification.flow_eq_loewnerMap_real line 260
  31. lemma OAI.SLEExactGauge.FlowIdentification.inverseFlow_eq_literal line 264
  32. lemma OAI.SLEExactGauge.FlowIdentification.trace_eq_literal line 274
  33. theorem OAI.SLEExactGauge.FlowIdentification.trace_regular_actual_domains line 282
  34. lemma OAI.SLEExactGauge.LoewnerScaling.brownian_map_inverse_driver line 322
  35. lemma OAI.SLEExactGauge.LoewnerScaling.brownian_evaluation_law_unique line 335
  36. lemma OAI.SLEExactGauge.LoewnerScaling.brownian_scaled line 342
  37. lemma OAI.SLEExactGauge.LoewnerScaling.brownian_map_scaled line 348
  38. lemma OAI.SLEExactGauge.LoewnerScaling.map_scaleDriver_eq line 361
  39. lemma OAI.SLEExactGauge.LoewnerScaling.measurePreserving_scaleDriver line 366
  40. lemma OAI.ExactSLEMain.odeUntil_join line 385
  41. theorem OAI.ExactSLEMain.alive_restart_iff line 444
  42. lemma OAI.ExactSLEMain.continuous_shiftDriver line 455
  43. lemma OAI.ExactSLEMain.deriv_loewnerMap_restart line 461