OAI/Probability/SLE/Gauge/PrescribedGridHeightSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the one-point height factor over the actual finite shifted grid. The constant depends on the bounded region, not on the mesh.

  1. lemma OAI.SLEExactGauge.int_row_sum line 14
  2. theorem OAI.SLEExactGauge.prescribed_grid_height_sum_bound line 21