CoverGrid.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A finite physical grid in a bounded disk, with the planar cell count needed by the missed-cell estimate. Closed disks are used as fine cells.

def OAI.SLEExactGauge.coverGridCenter line 14
def OAI.SLEExactGauge.coverGridIndex line 17
def OAI.SLEExactGauge.retainedCoverGridIndex line 21
lemma OAI.SLEExactGauge.coverGrid_coordinate line 26
lemma OAI.SLEExactGauge.coverGrid_floor_distance line 43
theorem OAI.SLEExactGauge.coverGrid_covers_disk line 70
theorem OAI.SLEExactGauge.coverGrid_card_bound line 82
Source documentation
The constant depends on the bounded disk, and not on the small mesh.
```
theorem coverGrid_card_bound {R r : ℝ} (hR : 0 ≤ R) (hr : 0 < r) (hr1 : r ≤ 1) :
    ((coverGridIndex R r).card : ℝ) ≤ (2 * R + 5) ^ 2 * r ^ (-2 : ℝ) := by
…
```
Mentions: OAI.SLEExactGauge.coverGridIndex
theorem OAI.SLEExactGauge.retainedCoverGrid_covers line 114
theorem OAI.SLEExactGauge.retainedCoverGrid_card_bound line 123

theorem OAI.SLEExactGauge.retainedCoverGrid_center_bounds line 131

Source documentation

Retaining only cells meeting the interior cutoff keeps all their centers away from the real boundary and in one fixed enlarged bounded disk.

theorem retainedCoverGrid_center_bounds {R r η : ℝ} {K : Set ℂ}
    (hK : K ⊆ closedBall 0 R) (hheight : ∀ z ∈ K, η ≤ z.im)
    {ij : ℤ × ℤ} (hij : ij ∈ retainedCoverGridIndex R r K) :
    ‖coverGridCenter r ij‖ ≤ R + 2 * r ∧
      η - 2 * r ≤ (coverGridCenter r ij).im := by
…

Mentions: OAI.SLEExactGauge.retainedCoverGridIndex, OAI.SLEExactGauge.coverGridCenter

lemma OAI.SLEExactGauge.coverGrid_cell_diameter line 152