OAI/Probability/SLEGauge/TwoPointGrowth.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEMain.loewner_two_point_growth line 22
  2. lemma OAI.ExactSLEMain.interaction_integral_strong line 129
  3. lemma OAI.ExactSLEMain.interaction_constant_comparison line 210
  4. theorem OAI.ExactSLEMain.weighted_interaction_integral line 227
  5. def OAI.ExactSLEMain.fullLoewnerRadius line 246
  6. def OAI.ExactSLEMain.odeSpeed line 250
  7. def OAI.ExactSLEMain.activeODEClock line 253
  8. lemma OAI.ExactSLEMain.odeSpeed_eq line 257
  9. lemma OAI.ExactSLEMain.odeSpeed_continuous line 261
  10. lemma OAI.ExactSLEMain.fullRadius_primitive line 269
  11. lemma OAI.ExactSLEMain.fullRadius_pos line 291
  12. lemma OAI.ExactSLEMain.fullRadius_active_clock line 297
  13. lemma OAI.ExactSLEMain.activeODEClock_deriv line 309
  14. lemma OAI.ExactSLEMain.activeODEClock_nonneg line 316
  15. lemma OAI.ExactSLEMain.neg_log_le_sqrt_ratio line 321
  16. lemma OAI.ExactSLEMain.log_sq_mul_le line 334
  17. lemma OAI.ExactSLEMain.ode_pair_ratio_pos_lt_one line 343
  18. lemma OAI.ExactSLEMain.actual_pair_clock_decay line 352
  19. lemma OAI.ExactSLEMain.ode_pair_log_deriv line 386
  20. theorem OAI.ExactSLEMain.actual_pair_interaction line 403