OAI/Probability/SLE/Gauge/SerpentineArrayRegion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Horizontal confinement of the whole infinite array. This keeps every part of the completed experiment away from the marked-point shadow.

  1. lemma OAI.SLEExactGauge.Serpentine.array_normal_re_lower line 13