OAI/Probability/SLE/Loewner/LoewnerTipHullApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Kernel convergence cannot leave a fixed surviving ball around the limiting tip. The boundary derivative estimate gives a quantitative contradiction to such a ball.

  1. theorem OAI.SLEExactGauge.inverse_convergence_excludes_common_tip_ball line 16
  2. theorem OAI.SLEExactGauge.driver_neighborhood_hits_tip_hull line 60