OAI/Probability/SLE/Loewner/SlitChartLimitUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of a terminal inverse-chart limit with the normalized static chart. Only the preserved height and far-field bounds are used.

  1. lemma OAI.SLEExactGauge.SimpleSlitChart.eq_inverse_of_vertical_bounds line 14
  2. theorem OAI.SLEExactGauge.initialInverse_limit_eq_final line 86