OAI/Probability/SLE/Gauge/SerpentineMarkedLocal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The explicit marked access guide meets a small corner-chart disk exactly along its real diameter. The distant terminal prefix is excluded quantitatively, so there are no nonlocal intersections.

  1. lemma OAI.SLEExactGauge.Serpentine.terminalAccess_distance line 16
  2. theorem OAI.SLEExactGauge.Serpentine.completeMarkedAccess_corner_iff line 24
  3. theorem OAI.SLEExactGauge.Serpentine.completeMarkedAccess_corner_nnreal_iff line 64
  4. lemma OAI.SLEExactGauge.Serpentine.completeMarkedAccess_upper line 76