UniformCoverLevels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform clock geometry over the moving grid centers retained above a fixed positive height. The terminal visit level is separated from every test endpoint by a full clock unit.

def OAI.SLEExactGauge.coverVisitLevel line 16

theorem OAI.SLEExactGauge.eventually_uniform_cover_levels line 21

Source documentation

One deterministic cutoff works for every point above the retained height and every test index, including the endpoint after the last test.

theorem eventually_uniform_cover_levels {T η : ℝ} (hT : 0 < T) (hη : 0 < η) :
    ∀ᶠ n : ℕ in atTop, ∀ z : ℂ, η / 2 ≤ z.im →
      (∀ j : ℕ, n / 3 ≤ j →
        coverLogLevel z T j = Real.log (2 * z.im) + T * (j : ℝ)) ∧
      coverLogLevel z T (2 * n / 3 + 1) + 1 ≤ coverVisitLevel z T n ∧
      4 * coverRadius T n ≤ z.im := by
…

Mentions: OAI.SLEExactGauge.coverLogLevel, OAI.SLEExactGauge.coverVisitLevel, OAI.SLEExactGauge.coverRadius

lemma OAI.SLEExactGauge.coverVisitLevel_nonneg_of_gap line 56
lemma OAI.SLEExactGauge.coverVisitLevel_radius line 64
Source documentation
The late visit level is the fixed multiple 512π r_n of the fine mesh, independently of the varying center's height.
```
lemma coverVisitLevel_radius (z : ℂ) (hz : 0 < z.im) (T : ℝ) (n : ℕ) :
    (2 * z.im) * Real.exp (-coverVisitLevel z T n) =
      (512 * Real.pi) * coverRadius T n := by
…
```
Mentions: OAI.SLEExactGauge.coverVisitLevel, OAI.SLEExactGauge.coverRadius

theorem OAI.SLEExactGauge.eventually_uniform_cover_window_levels line 79

Source documentation

The exact test window inherits the common late-grid cutoff.

theorem eventually_uniform_cover_window_levels {T η : ℝ} (hT : 0 < T) (hη : 0 < η) :
    ∀ᶠ n : ℕ in atTop, ∀ z : ℂ, η / 2 ≤ z.im →
      (∀ j ∈ coverTestWindow n,
        coverLogLevel z T j = Real.log (2 * z.im) + T * (j : ℝ)) ∧
      coverLogLevel z T (2 * n / 3 + 1) =
        Real.log (2 * z.im) + T * ((2 * n / 3 + 1 : ℕ) : ℝ) ∧
      coverLogLevel z T (2 * n / 3 + 1) + 1 ≤ coverVisitLevel z T n ∧
      4 * coverRadius T n ≤ z.im := by
…

Mentions: OAI.SLEExactGauge.coverTestWindow, OAI.SLEExactGauge.coverLogLevel, OAI.SLEExactGauge.coverVisitLevel, OAI.SLEExactGauge.coverRadius

theorem OAI.SLEExactGauge.eventually_retained_grid_cover_levels line 95
Source documentation
In particular the changing retained grid centers satisfy all clock and visit geometry simultaneously; no center-dependent cutoff is required.
```
theorem eventually_retained_grid_cover_levels {R T η : ℝ} {K : Set ℂ}
    (hT : 0 < T) (hη : 0 < η) (hK : K ⊆ Metric.closedBall 0 R)
    (hheight : ∀ z ∈ K, η ≤ z.im) :
    ∀ᶠ n : ℕ in atTop, ∀ ij ∈ retainedCoverGridIndex R (coverRadius T n) K,
      let z := coverGridCenter (coverRadius T n) ij
…
```
Mentions: OAI.SLEExactGauge.retainedCoverGridIndex, OAI.SLEExactGauge.coverRadius, OAI.SLEExactGauge.coverGridCenter