OAI/Probability/SLEGauge/ConformalRestartMap.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerRestart.literal_parameter line 18
  2. lemma OAI.SLEExactGauge.LoewnerRestart.literal_flow line 20
  3. lemma OAI.SLEExactGauge.LoewnerRestart.literal_surviving line 24
  4. def OAI.SLEExactGauge.LoewnerRestart.inverseMap line 29
  5. lemma OAI.SLEExactGauge.LoewnerRestart.inverseMap_alive line 32
  6. lemma OAI.SLEExactGauge.LoewnerRestart.alive_initial_im line 38
  7. lemma OAI.SLEExactGauge.LoewnerRestart.loewnerMap_im_pos line 43
  8. lemma OAI.SLEExactGauge.LoewnerRestart.centered_inverseMap line 49
  9. lemma OAI.SLEExactGauge.LoewnerRestart.inverseMap_centered line 55
  10. lemma OAI.SLEExactGauge.LoewnerRestart.inverseMap_hasStrictDerivAt line 61
  11. lemma OAI.SLEExactGauge.LoewnerRestart.deriv_inverseMap line 72
  12. lemma OAI.SLEExactGauge.LoewnerRestart.deriv_inverseMap_ne_zero line 77
  13. def OAI.SLEExactGauge.LoewnerRestart.inverseUpper line 83
  14. lemma OAI.SLEExactGauge.LoewnerRestart.continuous_inverseUpper line 86
  15. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_injective line 94
  16. def OAI.SLEExactGauge.LoewnerRestart.restartHomeomorph line 102
  17. abbrev OAI.SLEExactGauge.LoewnerRestart.AliveData line 138
  18. def OAI.SLEExactGauge.LoewnerRestart.centeredData line 141
  19. lemma OAI.SLEExactGauge.LoewnerRestart.measurable_centeredData line 145
  20. lemma OAI.SLEExactGauge.LoewnerRestart.centeredData_injective line 154
  21. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_joint_measurable line 168
  22. lemma OAI.SLEExactGauge.LoewnerRestart.norm_deriv_inverseMap_eq_exp line 192
  23. lemma OAI.SLEExactGauge.LoewnerRestart.norm_deriv_inverseMap_joint_measurable line 202
  24. def OAI.SLEExactGauge.Conformal.realDerivative line 224
  25. lemma OAI.SLEExactGauge.Conformal.det_realDerivative line 227
  26. lemma OAI.SLEExactGauge.Conformal.lintegral_image_complex line 231
  27. lemma OAI.SLEExactGauge.Conformal.map_withDensity_composed line 242
  28. def OAI.SLEExactGauge.LoewnerRestart.upperExtend line 266
  29. lemma OAI.SLEExactGauge.LoewnerRestart.upperExtend_coe line 269
  30. lemma OAI.SLEExactGauge.LoewnerRestart.image_inverseMap_upper line 272
  31. lemma OAI.SLEExactGauge.LoewnerRestart.inverseMap_injOn_upper line 284
  32. theorem OAI.SLEExactGauge.LoewnerRestart.inverseUpper_lintegral_area line 292
  33. theorem OAI.SLEExactGauge.LoewnerRestart.map_inverseUpper_area line 313
  34. def OAI.SLEExactGauge.LoewnerRestart.restartWeight line 355
  35. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_pos line 358
  36. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_ne_top line 362
  37. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_joint_measurable line 365
  38. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_measurable line 369
  39. lemma OAI.SLEExactGauge.LoewnerRestart.green_jacobian_restart line 377
  40. theorem OAI.SLEExactGauge.LoewnerRestart.inverseUpper_lintegral_green line 399
  41. def OAI.SLEExactGauge.LoewnerRestart.restartPush line 411
  42. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_lintegral line 414
  43. theorem OAI.SLEExactGauge.LoewnerRestart.restartPush_survivingKernel line 426
  44. lemma OAI.SLEExactGauge.LoewnerRestart.inverseMap_driver_congr line 475
  45. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_driver_congr line 487
  46. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_driver_congr line 493
  47. def OAI.SLEExactGauge.LoewnerRestart.stoppedData line 501
  48. lemma OAI.SLEExactGauge.LoewnerRestart.stoppedData_raw_measurable line 504
  49. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_stoppedData line 510
  50. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_stoppedData line 515
  51. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_stopped_raw_joint line 520
  52. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_stopped_raw_joint line 533