OAI/Probability/SLE/Angle/TargetDiskVisit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed relative half-plane ball lies inside the prescribed disk compact. Reaching a sufficiently small radius level forces a positive-time visit there.

  1. lemma OAI.SLEExactGauge.Target.diskMapInv_zero line 15
  2. lemma OAI.SLEExactGauge.Target.marked_ball_subset_diskSource line 18
  3. lemma OAI.SLEExactGauge.Target.radius_level_visits_diskSource line 42