OAI/Probability/SLE/Gauge/SerpentineRetainedStrips.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prescribed integer middle strips are actual straight portions of the joined serpentine, with exactly m² distinct retained indices.

  1. lemma OAI.SLEExactGauge.Serpentine.columnEntry_mono line 15
  2. lemma OAI.SLEExactGauge.Serpentine.array_preserves_column line 22
  3. lemma OAI.SLEExactGauge.Serpentine.array_on_column line 46
  4. lemma OAI.SLEExactGauge.Serpentine.complete_normal_on_column line 54
  5. lemma OAI.SLEExactGauge.Serpentine.retained_strip_on_column line 70