MissedCellCleanup.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The planar grid count cancels the gauge and hitting exponents in the missed-cell contribution to the dense cover.

theorem OAI.SLEExactGauge.missed_cell_sum_bound line 14

theorem OAI.SLEExactGauge.missed_cell_sum_tendsto_zero line 53

Source documentation

The missed-cell cost vanishes even when its finite prefactor depends on the compact interior cutoff. The leading sausage charge does not depend on it.

theorem missed_cell_sum_tendsto_zero {ι : Type*}
    (I : ℕ → Finset ι) (cost prob : ℕ → ι → ℝ≥0∞)
    (κ : ℝ) (hκ : 0 < κ) (r : ℕ → ℝ) (hr : ∀ n, 0 < r n)
    (c : ℝ) (hc : 0 < c) (A B D : ℝ)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hD : 0 ≤ D)
    (hcard : ∀ n, ((I n).card : ℝ) ≤ A * r n ^ (-2 : ℝ))
    (hcost : ∀ n i, i ∈ I n → cost n i ≤ ENNReal.ofReal
      (B * r n ^ dimension κ * (Real.log (n : ℝ)) ^ (codimension κ / 2)))
    (hprob : ∀ n i, i ∈ I n → prob n i ≤ ENNReal.ofReal
      (D * r n ^ codimension κ * Real.exp (-c * Real.sqrt (n : ℝ)))) :
    Tendsto (fun n => ∑ i ∈ I n, cost n i * prob n i) atTop (𝓝 0) := by
…

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