OAI/Probability/SLE/Loewner/SlitChartProper.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalization at infinity prevents bounded physical points from having unbounded chart coordinates, including when they approach the slit.

  1. lemma OAI.SLEExactGauge.SimpleSlitChart.forward_bounded_over_ball line 13