OAI/Probability/SLE/Gauge/DenseInfinityCriterion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A countable test for a continuous function's limit at infinity on an open planar domain. Only the values on one fixed dense sequence are used.

  1. def OAI.SLEExactGauge.DenseInfinityCriterion line 13
  2. lemma OAI.SLEExactGauge.denseInfinityCriterion_of_tendsto line 18
  3. lemma OAI.SLEExactGauge.DenseInfinityCriterion.bound line 28
  4. lemma OAI.SLEExactGauge.DenseInfinityCriterion.tendsto line 45