OAI/Probability/SLE/Geometry/MarkedAccessHook.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A proper polygonal continuation from the high right-hand tail of the serpentine through the marked point and then to infinity on its left.

  1. def OAI.SLEExactGauge.Serpentine.hookTop line 15
  2. def OAI.SLEExactGauge.Serpentine.hookDown line 17
  3. def OAI.SLEExactGauge.Serpentine.hookLeft line 20
  4. def OAI.SLEExactGauge.Serpentine.hookUp line 23
  5. def OAI.SLEExactGauge.Serpentine.markedHook line 26
  6. lemma OAI.SLEExactGauge.Serpentine.markedHook_zero line 31
  7. lemma OAI.SLEExactGauge.Serpentine.markedHook_continuous line 36
  8. lemma OAI.SLEExactGauge.Serpentine.markedHook_pieces line 64
  9. lemma OAI.SLEExactGauge.Serpentine.markedHook_injective line 86
  10. lemma OAI.SLEExactGauge.Serpentine.markedHook_passes_marked line 101
  11. lemma OAI.SLEExactGauge.Serpentine.markedHook_tail_region line 109
  12. lemma OAI.SLEExactGauge.Serpentine.markedHook_disjoint_prefix line 126
  13. lemma OAI.SLEExactGauge.Serpentine.markedHook_tail line 135
  14. lemma OAI.SLEExactGauge.Serpentine.markedHook_unbounded line 142
  15. theorem OAI.SLEExactGauge.Serpentine.markedHook_survives line 160
  16. def OAI.SLEExactGauge.Serpentine.appendMarkedHook line 176
  17. lemma OAI.SLEExactGauge.Serpentine.appendMarkedHook_continuous line 179
  18. lemma OAI.SLEExactGauge.Serpentine.appendMarkedHook_injective line 187
  19. lemma OAI.SLEExactGauge.Serpentine.appendMarkedHook_passes_marked line 225