CoverNumerics.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The failure and residual-cover estimates used by the explicit gauge.

lemma OAI.SLEExactGauge.dense_cover_power_cancellation line 14
Source documentation
The dimensions in the hit probability, covering cost, and grid count cancel.
```
lemma dense_cover_power_cancellation (κ : ℝ) {r : ℝ} (hr : 0 < r) :
    r ^ (-2 : ℝ) * r ^ dimension κ * r ^ codimension κ = 1 := by
…
```
Mentions: OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension
lemma OAI.SLEExactGauge.failure_product_le_exp line 22
theorem OAI.SLEExactGauge.failure_window_le_stretchedExp line 31
Source documentation
A linear number of tests, each succeeding with probability at least n^(-1/2), has the stretched-exponential failure bound used in the paper.
```
theorem failure_window_le_stretchedExp {n : ℝ} (hn : 1 ≤ n)
    (N : ℕ) (hN : n / 4 ≤ (N : ℝ)) :
    (1 - 1 / Real.sqrt n) ^ N ≤ Real.exp (-Real.sqrt n / 4) := by
…
```
theorem OAI.SLEExactGauge.logarithmic_cleanup_tendsto_zero line 50
Source documentation
A logarithmic correction cannot offset the stretched-exponential failure probability obtained from the finite sequence of adapted tests.
```
theorem logarithmic_cleanup_tendsto_zero {q c : ℝ}
    (hq : q ≤ 1) (hc : 0 < c) :
    Tendsto (fun x : ℝ => (Real.log x) ^ q * Real.exp (-c * Real.sqrt x))
      atTop (𝓝 0) := by
…
```
theorem OAI.SLEExactGauge.explicit_cleanup_tendsto_zero line 74

theorem OAI.SLEExactGauge.expected_missed_cell_cost line 84

Source documentation

Finite expected residual cost is the sum of each missed-cell probability times its deterministic covering cost.

theorem expected_missed_cell_cost
    {Ω ι : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (I : Finset ι) (missed : ι → Set Ω)
    (hm : ∀ i ∈ I, MeasurableSet (missed i))
    (cost bound : ι → ℝ≥0∞)
    (hb : ∀ i ∈ I, P (missed i) ≤ bound i) :
    (∫⁻ ω, ∑ i ∈ I, (missed i).indicator (fun _ => cost i) ω ∂P) ≤
      ∑ i ∈ I, cost i * bound i := by
…