OAI/Probability/SLE/Gauge/SerpentineHorizontalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The whole completed physical ribbon stays between the exterior vertical lines x=-2 and x=2.

  1. lemma OAI.SLEExactGauge.Serpentine.array_normal_re_upper line 13
  2. lemma OAI.SLEExactGauge.Serpentine.lowConnector_re_bounds line 43
  3. lemma OAI.SLEExactGauge.Serpentine.lowConnector_normal_re_bounds line 67