CoverGaugeBounds.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The uniform gauge cost estimate in the finite-cover step of prop:dense-cover-upper, An explicit exact Hausdorff gauge for SLE. The window starts at floor (n / 3); the intermediate estimate uses n / 4 so it also covers that endpoint once n is large.

def OAI.SLEExactGauge.CoverGaugeBounds.radius line 20
lemma OAI.SLEExactGauge.CoverGaugeBounds.radius_pos line 22
lemma OAI.SLEExactGauge.CoverGaugeBounds.exp_scale_tendsto_zero line 24
lemma OAI.SLEExactGauge.CoverGaugeBounds.radius_tendsto_zero line 29
lemma OAI.SLEExactGauge.CoverGaugeBounds.scaled_quarter_radius_tendsto_zero line 33
lemma OAI.SLEExactGauge.CoverGaugeBounds.logLog_scaled_radius line 43

lemma OAI.SLEExactGauge.CoverGaugeBounds.formula_bound line 52

Source documentation

Once the clock argument is at least e, its log-log factor is bounded by (2 log n)^q uniformly for every index below n.

lemma formula_bound {κ C T n j : ℝ} (hκ8 : κ < 8) (hC : 0 < C)
    (hT : 0 < T) (hn : 1 ≤ n) (hN : T + |Real.log C| ≤ n)
    (hj : j ≤ n) (harg : Real.exp 1 ≤ T * j - Real.log C) :
    hFormula κ (C * Real.exp (-T * j)) ≤
      (C ^ dimension κ * (2 : ℝ) ^ (codimension κ / 2)) *
        Real.exp (-T * j) ^ dimension κ * (Real.log n) ^ (codimension κ / 2) := by
…

Mentions: OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension

theorem OAI.SLEExactGauge.CoverGaugeBounds.eventual_window_bound line 90

Source documentation

The selected disks' diameter costs have one uniform constant across the whole linear window of clock indices.

theorem eventual_window_bound {κ C T : ℝ} (hκ8 : κ < 8) (hC : 0 < C) (hT : 0 < T)
    {h : ℝ → ℝ} (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ A : ℝ, 0 < A ∧ ∀ᶠ n : ℕ in atTop, ∀ j : ℕ,
      (n : ℝ) / 4 ≤ (j : ℝ) → j ≤ n →
      h (C * radius T j) ≤ A * radius T j ^ dimension κ *
        (Real.log (n : ℝ)) ^ (codimension κ / 2) := by
…

Mentions: OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.CoverGaugeBounds.radius, OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension

lemma OAI.SLEExactGauge.CoverGaugeBounds.quarter_le_floor_third line 121

theorem OAI.SLEExactGauge.CoverGaugeBounds.eventual_floor_window_bound line 129

Source documentation

The source uses J₀ = floor (n/3), so the endpoint is included in the uniform estimate rather than silently replaced by n/3.

theorem eventual_floor_window_bound {κ C T : ℝ} (hκ8 : κ < 8) (hC : 0 < C) (hT : 0 < T)
    {h : ℝ → ℝ} (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ A : ℝ, 0 < A ∧ ∀ᶠ n : ℕ in atTop, ∀ j : ℕ,
      ⌊(n : ℝ) / 3⌋₊ ≤ j → j ≤ n →
      h (C * radius T j) ≤ A * radius T j ^ dimension κ *
        (Real.log (n : ℝ)) ^ (codimension κ / 2) := by
…

Mentions: OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.CoverGaugeBounds.radius, OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension

theorem OAI.SLEExactGauge.CoverGaugeBounds.floor_window_diameter_tendsto_zero line 143
Source documentation
In particular the largest selected diameter, at the first tested clock index, tends to zero.
```
theorem floor_window_diameter_tendsto_zero {C T : ℝ} (hT : 0 < T) :
    Tendsto (fun n : ℕ => C * radius T ⌊(n : ℝ) / 3⌋₊) atTop (𝓝 0) := by
…
```
Mentions: OAI.SLEExactGauge.CoverGaugeBounds.radius