OAI/MeasureTheory/DyadicAvoidance/WindowTableModel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem310.FiniteTableModel.selectorEdge line 13

   Source documentation

   The nondefault child edge used by a selector table.

   def selectorEdge (P : Node M d) (i : Fin M) : List (Child M) :=
   …

   Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.Child

2. lemma OAI.Problem310.FiniteTableModel.selectorEdge_valid line 16
3. lemma OAI.Problem310.FiniteTableModel.leaf_valid line 24
4. def OAI.Problem310.FiniteTableModel.selectorEndpoints line 34

   Source documentation

   Canonical selector resolutions are the incoming window endpoints.

   def selectorEndpoints (W : WindowData (M + 1) d g r₀) : Node M d → Fin M → ℕ :=
   …

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

5. def OAI.Problem310.FiniteTableModel.terminalEndpoints line 38

   Source documentation

   Each terminal table uses its leaf's incoming-edge endpoint.

   def terminalEndpoints (W : WindowData (M + 1) d g r₀) : Leaf M d → ℕ :=
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.FiniteTableModel.Leaf

6. lemma OAI.Problem310.FiniteTableModel.selectorEndpoints_descendant_le line 41
7. lemma OAI.Problem310.FiniteTableModel.terminalEndpoints_descendant_le line 48
8. lemma OAI.Problem310.FiniteTableModel.incoming_le_terminalEndpoints line 54
9. lemma OAI.Problem310.FiniteTableModel.selectorEndpoints_self_le line 62
10. lemma OAI.Problem310.FiniteTableModel.child_window_length line 68
11. lemma OAI.Problem310.FiniteTableModel.selector_window_endpoint line 73