GridStabilityFin.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.gridStableCenters_preserves_fin line 12

Source documentation

Bridge from quantitative stability to the canonical finite selector addresses.

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

Mentions: OAI.Problem310.gridStableCenters, OAI.Problem310.GridSeparation.dyadicKey

theorem OAI.Problem310.exists_uniform_grid_stability line 23

Source documentation

Choose the gap using only the finite number of grids, before their resolutions are assigned. Every subsequent assignment has a periodic measurable stable set with the same prescribed exceptional-density budget.

theorem exists_uniform_grid_stability {ι : Type u_ι} [Fintype ι]
    (p : ℝ) (hp : 0 < p) :
    ∃ g : ℕ, 2 ≤ g ∧ ∀ b : ι → ℕ, ∃ G : Set ℝ,
      MeasurableSet G ∧ (∀ x : ℝ, x + 1 ∈ G ↔ x ∈ G) ∧
      MeasureTheory.volume (Gᶜ ∩ Set.Icc (0 : ℝ) 1) ≤ ENNReal.ofReal p ∧
      ∀ x ∈ G, ∀ i : ι, ∀ n : ℕ, b i + g + 1 ≤ n →
        ∀ t ∈ Set.Icc (1 : ℝ) 2,
          GridSeparation.dyadicKey (b i) (x + t * ((2 : ℝ)⁻¹) ^ n) =
            GridSeparation.dyadicKey (b i) x := by
…

Mentions: OAI.Problem310.GridSeparation.dyadicKey