OAI/MeasureTheory/DyadicAvoidance/StableKeyRouting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.StableKeyRouting.selectorValue_eq_of_own_key_eq line 15

   Source documentation

   Agreement of the precise table key is enough to preserve a total selector lookup; nodes outside the finite routing tree consult no table.

   theorem selectorValue_eq_of_own_key_eq (b : Node M d → Fin M → ℕ)
       (ω : SelectorTable b) (P : List (Child M)) (i : Fin M) (x y : ℝ)
       (hkey : ∀ h : P.length < d,
         GridSeparation.dyadicKey (b ⟨P, h⟩ i) x = GridSeparation.dyadicKey (b ⟨P, h⟩ i) y) :
       selectorValue b ω P i x = selectorValue b ω P i y := by
   …

   Mentions: OAI.Problem310.GridSeparation.dyadicKey

2. theorem OAI.Problem310.StableKeyRouting.terminal_success_of_stable_keys line 30

   Source documentation

   Concrete finite-table version of the local-hit routing lemma. The geometric input is only equality of the grid keys used in earlier routing decisions.

   theorem terminal_success_of_stable_keys
       (b : Node M d → Fin M → ℕ) (ω : SelectorTable b)
       (terminal : List (Child M) → ℝ → Prop)
       (k r : ℕ) (P U : List (Child M)) (x y : ℝ) (i : Fin M)
       (hU : routeFrom (select (selectorValue b ω)) k P x = U)
       (hnd : ∀ l < k,
         select (selectorValue b ω) (routeFrom (select (selectorValue b ω)) l P x) x ≠ Fin.last M)
       (hprefix : ∀ l < k, ∀ j : Fin M,
         j.castSucc ≤ select (selectorValue b ω)
           (routeFrom (select (selectorValue b ω)) l P x) x →
         ∀ h : (routeFrom (select (selectorValue b ω)) l P x).length < d,
         GridSeparation.dyadicKey
   …

   Mentions: OAI.Problem310.GridSeparation.dyadicKey