OAI/MeasureTheory/DyadicAvoidance/WindowTrialAddresses.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem310.WindowTrialAddresses.LocalTrial line 14
2. def OAI.Problem310.WindowTrialAddresses.localStarts line 17
3. def OAI.Problem310.WindowTrialAddresses.localIndex line 20
4. theorem OAI.Problem310.WindowTrialAddresses.card_localTrial line 23
5. theorem OAI.Problem310.WindowTrialAddresses.localIndex_bounds line 27
6. def OAI.Problem310.WindowTrialAddresses.localSelectorAddress line 37

   Source documentation

   The actual finite-model selector coordinate read at one child-window trial.

   def localSelectorAddress (W : WindowData (M + 1) d g r₀) (P : Node M d)
       (x t : ℝ) (z : LocalTrial W P) : SelectorAddress (selectorEndpoints W) :=
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.WindowTrialAddresses.LocalTrial

7. theorem OAI.Problem310.WindowTrialAddresses.localSelectorAddress_injective line 42
8. theorem OAI.Problem310.WindowTrialAddresses.localSelectorAddress_ne_center line 54
9. theorem OAI.Problem310.WindowTrialAddresses.center_local_sum_injective line 67

   Source documentation

   This is the single address-injectivity assumption needed by center exposure: every center coordinate and every local trial coordinate are fresh.

   theorem center_local_sum_injective (W : WindowData (M + 1) d g r₀)
       (P : Node M d) (x t : ℝ) (ht : t ∈ Set.Icc (1 : ℝ) 2) :
       Function.Injective (Sum.elim
         (fun e : Node M d × Fin M => selectorAddress (selectorEndpoints W) e.1 e.2 x)
         (localSelectorAddress W P x t)) := by
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.WindowTrialAddresses.localSelectorAddress

10. theorem OAI.Problem310.WindowTrialAddresses.localTerminalAddress_injective line 90

    Source documentation

    Once local routing stays in its chosen child subtree, all terminal coordinates are distinct. WindowData automatically supplies the necessary resolution refinement, so no numerical hypothesis remains.

    theorem localTerminalAddress_injective (W : WindowData (M + 1) d g r₀)
        (P : Node M d) (x t : ℝ) (ht : t ∈ Set.Icc (1 : ℝ) 2)
        (leaf : LocalTrial W P → Leaf M d)
        (hprefix : ∀ z, (selectorEdge P z.1).IsPrefix (leaf z).val) :
        Function.Injective (fun z : LocalTrial W P =>
          terminalAddress (terminalEndpoints W) (leaf z)
            (x + t * ((2 : ℝ)⁻¹ ^ localIndex W P z))) := by
    …

    Mentions: OAI.Problem310.WindowData, OAI.Problem310.WindowTrialAddresses.LocalTrial, OAI.Problem310.WindowTrialAddresses.localIndex