OAI/Probability/SLELocalization/FirstDisk.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Is Loewner Trace Using estimates.

  1. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.hasDerivAt_real line 18
  2. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.initial_real_le line 25
  3. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.initial_real_ge line 52
  4. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.initial_height_sq_le line 82
  5. theorem OAI.SLEExactGauge.trace_driver_rectangle line 120
  6. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.earlier_real_le line 169
  7. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.earlier_real_ge line 197
  8. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.earlier_height_sq_le line 228
  9. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.later_real_le line 255
  10. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.later_real_ge line 281
  11. theorem OAI.SLEExactGauge.IsLoewnerTraceUsing.earlier_tip_rectangle line 309
  12. lemma OAI.SLEExactGauge.ball_subset_localizationDomain line 357
  13. lemma OAI.SLEExactGauge.first_disk_hit_free line 368
  14. lemma OAI.SLEExactGauge.first_disk_hit_live_before line 391
  15. theorem OAI.SLEExactGauge.IsLoewnerTraceUsing.fresh_tip_access line 413
  16. theorem OAI.SLEExactGauge.first_disk_hit_access line 489
  17. theorem OAI.SLEExactGauge.first_disk_hit_access_path line 499