GridStability.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.gridStableCenters line 13
Source documentation
Simultaneous stable centers for a finite list of earlier-grid/later-window pairs.
```
def gridStableCenters {ι : Type u_ι} (a b : ι → ℕ) : Set ℝ :=
…
```
theorem OAI.Problem310.measurableSet_gridStableCenters line 16
theorem OAI.Problem310.gridStableCenters_add_one line 23

theorem OAI.Problem310.gridStableCenters_preserves line 31

Source documentation

Stability at a grid also preserves every coarser grid at a later-window trial.

theorem gridStableCenters_preserves {ι : Type u_ι} {a b : ι → ℕ} {x t : ℝ}
    (hx : x ∈ gridStableCenters a b) (i : ι) {c n : ℕ}
    (hc : c ≤ b i) (hn : a i ≤ n) (ht : t ∈ Icc (1 : ℝ) 2) :
    dyadicGridKey c (x + t * ((2 : ℝ)⁻¹) ^ n) = dyadicGridKey c x := by
…

Mentions: OAI.Problem310.gridStableCenters, OAI.Problem310.dyadicGridKey

theorem OAI.Problem310.grid_window_width_le line 45

theorem OAI.Problem310.volume_gridStableCenters_compl_period_le line 59

Source documentation

A quantitative simultaneous stability estimate, with no tree assumptions.

theorem volume_gridStableCenters_compl_period_le {ι : Type u_ι} [Fintype ι]
    (a b : ι → ℕ) (hgap : ∀ i, b i + 3 ≤ a i) :
    volume ((gridStableCenters a b)ᶜ ∩ Icc (0 : ℝ) 1) ≤
      ENNReal.ofReal (∑ i, (2 : ℝ) ^ (b i + 2) * (2 * ((2 : ℝ)⁻¹) ^ (a i))) := by
…

Mentions: OAI.Problem310.gridStableCenters

theorem OAI.Problem310.dyadic_grid_gap_budget line 70
Source documentation
The density cost of a gap depends only on its length, not on the grid resolution.
```
theorem dyadic_grid_gap_budget (b g : ℕ) :
    (2 : ℝ) ^ (b + 2) * (2 * ((2 : ℝ)⁻¹) ^ (b + g + 1)) =
      4 * ((2 : ℝ)⁻¹) ^ g := by
…
```
theorem OAI.Problem310.volume_gridStableCenters_compl_gap_le line 84

theorem OAI.Problem310.volume_gridStableCenters_compl_gap_le_of_le line 97

Source documentation

The same bound holds when windows are separated by at least the chosen gap. This can be indexed by all ordered pairs of windows, not just predecessor pairs.

theorem volume_gridStableCenters_compl_gap_le_of_le {ι : Type u_ι} [Fintype ι]
    (a b : ι → ℕ) (g : ℕ) (hg : 2 ≤ g)
    (ha : ∀ i, b i + g + 1 ≤ a i) :
    volume ((gridStableCenters a b)ᶜ ∩ Icc (0 : ℝ) 1) ≤
      ENNReal.ofReal ((Fintype.card ι : ℝ) * (4 * ((2 : ℝ)⁻¹) ^ g)) := by
…

Mentions: OAI.Problem310.gridStableCenters

theorem OAI.Problem310.exists_dyadic_gap_budget line 122
Source documentation
Any prescribed finite number of stability conditions has arbitrarily small exceptional density once the unused gap is sufficiently long.
```
theorem exists_dyadic_gap_budget (K : ℕ) {p : ℝ} (hp : 0 < p) :
    ∃ g : ℕ, 2 ≤ g ∧ (K : ℝ) * (4 * ((2 : ℝ)⁻¹) ^ g) < p := by
…
```