OAI/MeasureTheory/DyadicAvoidance/WindowDataStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.exists_windowData_selector_stability line 15

   Source documentation

   Actual selector stability for arbitrary canonical window data. The gap is chosen before the window recursion and all its resolutions. Prefix and sibling gap fields of W may be applied directly to the displayed strict cutoff.

   theorem exists_windowData_selector_stability (M d : ℕ) (p : ℝ) (hp : 0 < p) :
       ∃ g : ℕ, 2 ≤ g ∧ ∀ r₀ : ℕ, ∀ W : WindowData (M + 1) d g r₀,
         ∃ G : Set ℝ, MeasurableSet G ∧
           (∀ x : ℝ, x + 1 ∈ G ↔ x ∈ G) ∧
           MeasureTheory.volume (Gᶜ ∩ Set.Icc (0 : ℝ) 1) ≤ ENNReal.ofReal p ∧
           ∀ x ∈ G, ∀ P : Node M d, ∀ i : Fin M, ∀ n : ℕ,
             W.b (P.val ++ [i.castSucc]) + g < n →
             ∀ t ∈ Set.Icc (1 : ℝ) 2,
             ∀ ω : SelectorTable (fun P : Node M d => fun i : Fin M =>
               W.b (P.val ++ [i.castSucc])),
             selectorValue (fun P : Node M d => fun i : Fin M =>
               W.b (P.val ++ [i.castSucc])) ω P.val i (x + t * ((2 : ℝ)⁻¹) ^ n) =
   …

   Mentions: OAI.Problem310.WindowData