OAI/Probability/SLE/Gauge/PrescribedCoverGrid.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The final mesh is shifted by half a row. Every retained center is in the open half-plane, while its closed cell can cover the real boundary.

  1. def OAI.SLEExactGauge.prescribedGridCenter line 13
  2. def OAI.SLEExactGauge.prescribedFineCell line 16
  3. def OAI.SLEExactGauge.prescribedGridIndex line 19
  4. lemma OAI.SLEExactGauge.prescribedGrid_floor_distance line 24
  5. lemma OAI.SLEExactGauge.prescribedGrid_covers line 34
  6. lemma OAI.SLEExactGauge.prescribedGrid_center_height line 49
  7. lemma OAI.SLEExactGauge.prescribedGrid_center_bound line 62
  8. lemma OAI.SLEExactGauge.prescribedGrid_card_bound line 74