OAI/MeasureTheory/DyadicAvoidance/WindowLocalHit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.WindowLocalHit.ancestor_selector_gap line 20

   Source documentation

   Every selector used at an earlier routed node precedes an incoming edge below that route, provided its child index is no later than the chosen child.

   theorem ancestor_selector_gap (W : WindowData q d g r₀)
       (choose : List (Fin q) → X → Fin q) (x : X)
       {k l : ℕ} (hkl : k < l) (hld : l < d) (i j : Fin q)
       (hj : j ≤ choose (routeFrom choose k [] x) x) :
       W.b (routeFrom choose k [] x ++ [j]) + g <
         W.a (routeFrom choose l [] x ++ [i]) := by
   …

   Mentions: OAI.Problem310.WindowData

2. theorem OAI.Problem310.WindowLocalHit.selectorValue_factors_window_key line 60

   Source documentation

   Canonical finite-table selectors satisfy the key-factor hypothesis of the window-routing lemma whenever their endpoint map is taken from W.

   theorem selectorValue_factors_window_key (W : WindowData (M + 1) d g r₀)
       (bS : FiniteTableModel.Node M d → Fin M → ℕ)
       (ωS : FiniteTableModel.SelectorTable bS)
       (hbS : ∀ (P : FiniteTableModel.Node M d) (j : Fin M),
         bS P j = W.b (P.val ++ [j.castSucc]))
       (P : List (Fin (M + 1))) (hP : P.length < d) (j : Fin M) (u v : ℝ)
       (hkey : dyadicKey (W.b (P ++ [j.castSucc])) u =
         dyadicKey (W.b (P ++ [j.castSucc])) v) :
       FiniteTableModel.selectorValue bS ωS P j u =
         FiniteTableModel.selectorValue bS ωS P j v := by
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.selectorValue

3. theorem OAI.Problem310.WindowLocalHit.route_eq_local_of_window_stability line 80

   Source documentation

   The actual window geometry turns uniform stable-grid agreement into the local-route identity at a first-default node. This is the concrete geometric input to the local-hit implication; no probability assumptions are used.

   theorem route_eq_local_of_window_stability (W : WindowData (M + 1) d g r₀)
       (S : List (Fin (M + 1)) → Fin M → ℝ → Bool)
       (hS : ∀ (P : List (Fin (M + 1))), P.length < d →
         ∀ (j : Fin M) (u v : ℝ),
           dyadicKey (W.b (P ++ [j.castSucc])) u =
             dyadicKey (W.b (P ++ [j.castSucc])) v → S P j u = S P j v)
       (x t : ℝ) (n k r : ℕ) (i : Fin M)
       (hdepth : k + 1 + r = d) (_ht : t ∈ Set.Icc (1 : ℝ) 2)
       (hn : n ∈ W.window (routeFrom (select S) k [] x ++ [i.castSucc]))
       (hstable : ∀ E : List (Fin (M + 1)), ValidWindowEdge d E →
         W.b E + g < n → dyadicKey (W.b E) x =
           dyadicKey (W.b E) (x + t * ((2 : ℝ)⁻¹ ^ n)))
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.ValidWindowEdge