OAI/Probability/SLEGauge/LoewnerSolutions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEMain.loewner_local_existence line 19
  2. def OAI.ExactSLEMain.heightClamp line 102
  3. lemma OAI.ExactSLEMain.heightClamp_eq line 104
  4. lemma OAI.ExactSLEMain.heightClamp_lipschitz line 107
  5. def OAI.ExactSLEMain.cutoffVector line 125
  6. lemma OAI.ExactSLEMain.cutoffVector_bound line 127
  7. lemma OAI.ExactSLEMain.cutoffVector_lipschitz line 133
  8. theorem OAI.ExactSLEMain.exists_cutoff_loewner line 151
  9. lemma OAI.ExactSLEMain.cutoff_loewner_hasDerivWithinAt line 167
  10. lemma OAI.ExactSLEMain.cutoff_loewner_dist line 180
  11. lemma OAI.ExactSLEMain.cutoff_loewner_eq_solution line 214
  12. theorem OAI.ExactSLEMain.loewner_local_cutoff line 235
  13. lemma OAI.ExactSLEMain.isOpen_alive line 286
  14. lemma OAI.ExactSLEMain.continuousAt_loewnerMap line 293
  15. lemma OAI.ExactSLEMain.scalar_linear_solution line 310
  16. lemma OAI.ExactSLEMain.scalar_linear_solution_on line 330
  17. theorem OAI.ExactSLEMain.loewner_solution_difference line 346
  18. lemma OAI.ExactSLEMain.heightClamp_norm_lower line 385
  19. lemma OAI.ExactSLEMain.heightClamp_ne_zero line 388
  20. lemma OAI.ExactSLEMain.invprod_heightClamp_bound line 391
  21. lemma OAI.ExactSLEMain.cutoff_loewner_continuous_start line 398