OAI/MeasureTheory/DyadicAvoidance/GridWindowStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.exists_window_stability line 11

   Source documentation

   Uniform stability for a finite sequence of windows. The gap is selected before any window lengths are fixed.

   theorem exists_window_stability (K : ℕ) (p : ℝ) (hp : 0 < p) :
       ∃ g : ℕ, 2 ≤ g ∧ ∀ len : ℕ → ℕ, ∃ G : Set ℝ,
         MeasurableSet G ∧ (∀ x : ℝ, x + 1 ∈ G ↔ x ∈ G) ∧
         MeasureTheory.volume (Gᶜ ∩ Set.Icc (0 : ℝ) 1) ≤ ENNReal.ofReal p ∧
         ∀ x ∈ G, ∀ f e : ℕ, f < e → e < K →
           ∀ n ∈ WindowPlacement.window len g e, ∀ t ∈ Set.Icc (1 : ℝ) 2,
             GridSeparation.dyadicKey (WindowPlacement.finish len g f)
               (x + t * ((2 : ℝ)⁻¹) ^ n) =
             GridSeparation.dyadicKey (WindowPlacement.finish len g f) x := by
   …

   Mentions: OAI.Problem310.WindowPlacement.window, OAI.Problem310.GridSeparation.dyadicKey, OAI.Problem310.WindowPlacement.finish