OAI/Probability/SLEGauge/AngleLyapunov.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEFiniteTilt.exists_tilted_coercivity line 19
  2. lemma OAI.ExactSLEGreen.physicalTheta_smooth_all line 65
  3. lemma OAI.ExactSLEGreen.physicalClock_smooth_all line 69
  4. lemma OAI.ExactSLEGreen.clockExp_smooth_all line 74
  5. lemma OAI.ExactSLEGreen.angleLift_sinePower_smooth_all line 78
  6. lemma OAI.ExactSLEGreen.green_exponential_angle_generator line 84
  7. def OAI.ExactSLEGreen.angleBudgetFactor line 102
  8. lemma OAI.ExactSLEGreen.angleBudgetFactor_smooth line 105
  9. lemma OAI.ExactSLEGreen.angleBudgetFactor_nonneg line 110
  10. lemma OAI.ExactSLEGreen.angleBudgetFactor_terminal line 124
  11. lemma OAI.ExactSLEGreen.green_angleBudget_generator line 131
  12. lemma OAI.ExactSLEGreen.green_angleBudget_generator_nonpos line 167
  13. theorem OAI.ExactSLEGenerator.compact_test_stopped_dynkin line 197
  14. def OAI.ExactSLEGreen.lifetimeCutoff line 258
  15. lemma OAI.ExactSLEGreen.lifetimeCutoff_smooth line 261
  16. lemma OAI.ExactSLEGreen.lifetimeCutoff_compact line 273
  17. lemma OAI.ExactSLEGreen.lifetimeCutoff_eq_near line 276
  18. def OAI.ExactSLEGreen.lifetimeCost line 282
  19. lemma OAI.ExactSLEGreen.lifetimeCost_pos line 285
  20. lemma OAI.ExactSLEGreen.lifetimeCost_continuousAt line 289
  21. lemma OAI.ExactSLEGreen.lifetimeCutoff_generator_le line 296
  22. theorem OAI.ExactSLEGreen.local_lifetime_budget line 310
  23. def OAI.ExactSLEGreen.angleBudgetCutoff line 427
  24. lemma OAI.ExactSLEGreen.angleBudgetCutoff_smooth line 430
  25. lemma OAI.ExactSLEGreen.angleBudgetCutoff_compact line 443
  26. lemma OAI.ExactSLEGreen.angleBudgetCutoff_eq_near line 447
  27. lemma OAI.ExactSLEGreen.angleBudgetCutoff_generator_nonpos line 453
  28. theorem OAI.ExactSLEGreen.local_angle_budget line 469