OAI/Probability/SLE/Geometry/MarkedSurvivingBall.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The marked corner lies in a quantitative free ball of the actual surviving component. This follows from the physical low-or-right geometry of the completed trace, with no filled-hull containment assumption.

  1. theorem OAI.SLEExactGauge.Serpentine.marked_ball_survives line 16
  2. lemma OAI.SLEExactGauge.Serpentine.marked_corner_ball_survives line 44