OAI/Combinatorics/MatrixRemoval/TreePositions.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Concrete depth-first orders for variable positions. Each class has 2^h positions. Classes 2*i and 2*i+1 are respectively plus and minus at i<h; class 2*h is the shared leaf class. The final two key components retain the original coordinates, making injectivity immediate without uniqueness assumptions on dyadic data.

  1. abbrev OAI.Problem348.TreePositions.VariablePosition line 15
  2. abbrev OAI.Problem348.TreePositions.OrderKey line 16
  3. def OAI.Problem348.TreePositions.key line 18
  4. def OAI.Problem348.TreePositions.earlyKey line 21
  5. def OAI.Problem348.TreePositions.lateKey line 24
  6. def OAI.Problem348.TreePositions.leafKey line 27
  7. def OAI.Problem348.TreePositions.orderKey line 31

    Source documentation

    column = false gives row order; true reverses the signs.

    def orderKey (column : Bool) (h : ℕ) (p : VariablePosition h) : OrderKey :=
…

    Mentions: OAI.Problem348.TreePositions.VariablePosition, OAI.Problem348.TreePositions.OrderKey

  8. abbrev OAI.Problem348.TreePositions.rowKey line 42
  9. abbrev OAI.Problem348.TreePositions.columnKey line 43
  10. def OAI.Problem348.TreePositions.keyClass line 45
  11. def OAI.Problem348.TreePositions.keyCoordinate line 46
  12. theorem OAI.Problem348.TreePositions.keyClass_key line 48
  13. theorem OAI.Problem348.TreePositions.keyCoordinate_key line 49
  14. theorem OAI.Problem348.TreePositions.keyClass_orderKey line 52
  15. theorem OAI.Problem348.TreePositions.keyCoordinate_orderKey line 57
  16. theorem OAI.Problem348.TreePositions.orderKey_injective line 62
  17. abbrev OAI.Problem348.TreePositions.positionOrder line 73

    Source documentation

    Explicit order structures, not global instances: the same raw positions carry different row and column orders.

    abbrev positionOrder (column : Bool) (h : ℕ) : LinearOrder (VariablePosition h) :=
…

    Mentions: OAI.Problem348.TreePositions.VariablePosition

  18. theorem OAI.Problem348.TreePositions.card_variablePosition line 76
  19. theorem OAI.Problem348.TreePositions.key_lt_iff_endpoint_le_of_tie_lt line 84
  20. theorem OAI.Problem348.TreePositions.lateKey_child_lt_parent line 89
  21. theorem OAI.Problem348.TreePositions.earlyKey_parent_lt_child line 97
  22. theorem OAI.Problem348.TreePositions.leafKey_lt_lateKey_parent line 109
  23. theorem OAI.Problem348.TreePositions.earlyKey_parent_lt_leafKey line 114
  24. def OAI.Problem348.TreePositions.plusPos line 121

    Source documentation

    The plus class; at depth h this is the shared leaf class.

    def plusPos {h : ℕ} (i : ℕ) (hi : i ≤ h) (x : Fin (2 ^ h)) : VariablePosition h :=
…

    Mentions: OAI.Problem348.TreePositions.VariablePosition

  25. def OAI.Problem348.TreePositions.minusPos line 125

    Source documentation

    The minus class, identified with the plus class exactly at the leaf.

    def minusPos {h : ℕ} (i : ℕ) (hi : i ≤ h) (x : Fin (2 ^ h)) : VariablePosition h :=
…

    Mentions: OAI.Problem348.TreePositions.VariablePosition

  26. def OAI.Problem348.TreePositions.node line 128
  27. theorem OAI.Problem348.TreePositions.minusPos_leaf line 130
  28. theorem OAI.Problem348.TreePositions.orderKey_leaf line 134
  29. theorem OAI.Problem348.TreePositions.rowKey_leaf line 138
  30. theorem OAI.Problem348.TreePositions.columnKey_leaf line 142
  31. theorem OAI.Problem348.TreePositions.rowKey_plus_internal line 146
  32. theorem OAI.Problem348.TreePositions.columnKey_plus_internal line 152
  33. theorem OAI.Problem348.TreePositions.rowKey_minus_internal line 158
  34. theorem OAI.Problem348.TreePositions.columnKey_minus_internal line 165
  35. theorem OAI.Problem348.TreePositions.row_plus_child_lt_parent line 177

    Source documentation

    The plus row-order equivalence, including shared leaves.

    theorem row_plus_child_lt_parent {h i : ℕ} (hi : i < h)
    (x y : Fin (2 ^ h)) :
    rowKey h (plusPos (i + 1) (by omega) x) <
        rowKey h (plusPos i (Nat.le_of_lt hi) y) ↔
      node (i + 1) x / 2 ≤ node i y := by
…

    Mentions: OAI.Problem348.TreePositions.rowKey, OAI.Problem348.TreePositions.plusPos, OAI.Problem348.TreePositions.node

  36. theorem OAI.Problem348.TreePositions.row_minus_parent_lt_child line 199

    Source documentation

    The minus row-order equivalence, including shared leaves.

    theorem row_minus_parent_lt_child {h i : ℕ} (hi : i < h)
    (x y : Fin (2 ^ h)) :
    rowKey h (minusPos i (Nat.le_of_lt hi) y) <
        rowKey h (minusPos (i + 1) (by omega) x) ↔
      node i y ≤ node (i + 1) x / 2 := by
…

    Mentions: OAI.Problem348.TreePositions.rowKey, OAI.Problem348.TreePositions.minusPos, OAI.Problem348.TreePositions.node

  37. theorem OAI.Problem348.TreePositions.column_plus_parent_lt_child line 221

    Source documentation

    The plus column-order equivalence, including shared leaves.

    theorem column_plus_parent_lt_child {h i : ℕ} (hi : i < h)
    (x y : Fin (2 ^ h)) :
    columnKey h (plusPos i (Nat.le_of_lt hi) y) <
        columnKey h (plusPos (i + 1) (by omega) x) ↔
      node i y ≤ node (i + 1) x / 2 := by
…

    Mentions: OAI.Problem348.TreePositions.columnKey, OAI.Problem348.TreePositions.plusPos, OAI.Problem348.TreePositions.node

  38. theorem OAI.Problem348.TreePositions.column_minus_child_lt_parent line 243

    Source documentation

    The minus column-order equivalence, including shared leaves.

    theorem column_minus_child_lt_parent {h i : ℕ} (hi : i < h)
    (x y : Fin (2 ^ h)) :
    columnKey h (minusPos (i + 1) (by omega) x) <
        columnKey h (minusPos i (Nat.le_of_lt hi) y) ↔
      node (i + 1) x / 2 ≤ node i y := by
…

    Mentions: OAI.Problem348.TreePositions.columnKey, OAI.Problem348.TreePositions.minusPos, OAI.Problem348.TreePositions.node