OAI/Probability/SLE/Gauge/PrescribedHeightSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform sums of the actual half-row heights, including a lower strip of arbitrary height. The bound is independent of the final mesh size.

  1. lemma OAI.SLEExactGauge.scaled_half_integer_row_sum line 13
  2. lemma OAI.SLEExactGauge.half_integer_lower_strip_sum line 34