OAI/Probability/SLEGauge/HeightRadius.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEBarrier.Evolution.logHeight_add_deriv line 19
  2. lemma OAI.ExactSLEBarrier.Evolution.logHeight_add_le line 27
  3. lemma OAI.ExactSLEBarrier.Evolution.height_sq_le_radius line 41
  4. lemma OAI.ExactSLEBarrier.Evolution.height_sq_lower line 54
  5. lemma OAI.ExactSLEGreen.actualState_evolution line 79
  6. lemma OAI.ExactSLEGreen.actual_height_sq_le_radius line 109
  7. lemma OAI.ExactSLEGreen.actual_height_sq_lower line 118
  8. lemma OAI.ExactSLEGreen.level_height_bound line 128
  9. lemma OAI.ExactSLEGreen.radialTime_half_lower line 148
  10. lemma OAI.SLEExactGauge.AnalyticCompactness.lipschitzOn_subball line 174
  11. theorem OAI.SLEExactGauge.AnalyticCompactness.exists_subseq_uniform line 202
  12. theorem OAI.SLEExactGauge.AnalyticCompactness.uniform_zero_of_accumulation line 245
  13. theorem OAI.SLEExactGauge.AnalyticCompactness.uniform_zero_on_horizontal line 286
  14. theorem OAI.SLEExactGauge.AngularLimits.uniform_angular_of_radial line 371
  15. theorem OAI.SLEExactGauge.TraceChaining.radial_uniform_limit_nhds_of_bands line 479
  16. theorem OAI.SLEExactGauge.LiteralTrace.radial_uniform_all_windows line 521
  17. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_shift_bound line 539
  18. theorem OAI.SLEExactGauge.LiteralTrace.angular_uniform_all_windows line 562