OAI/Probability/SLE/Gauge/SerpentineMarkedGuide.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The explicit complete physical access guide from the final ribbon tip, through the marked point, and then vertically to infinity.

  1. def OAI.SLEExactGauge.Serpentine.terminalAccess line 16
  2. def OAI.SLEExactGauge.Serpentine.completeMarkedAccess line 19
  3. lemma OAI.SLEExactGauge.Serpentine.terminalAccess_continuous line 23
  4. lemma OAI.SLEExactGauge.Serpentine.terminalAccess_right line 29
  5. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_continuous line 43
  6. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_injective line 55
  7. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_zero line 75
  8. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_hits_marked line 82
  9. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_norm_tendsto line 95