OAI/Combinatorics/MatrixRemoval/HostTreeOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Comparison lemmas for the concrete depth-first tree orders used in mode localization.

  1. theorem OAI.Problem348.Construction.eq_plusPos_of_atLevel line 15
  2. theorem OAI.Problem348.Construction.eq_minusPos_of_atLevel line 30
  3. theorem OAI.Problem348.Construction.node_eq_level_node line 47
  4. theorem OAI.Problem348.Construction.row_plus_lt_iff line 52

    Source documentation

    Row plus child precedes row plus parent exactly for the stated parent-node inequality.

    theorem row_plus_lt_iff {h i : ℕ} {child parent : VariablePosition h}
    (hc : AtLevel (i + 1) true child) (hp : AtLevel i true parent) :
    TreePositions.rowKey h child < TreePositions.rowKey h parent ↔
      node child / 2 ≤ node parent := by
…

    Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.TreePositions.rowKey, OAI.Problem348.Construction.node

  5. theorem OAI.Problem348.Construction.row_minus_lt_iff line 63

    Source documentation

    Row minus parent precedes row minus child exactly for the parent-node inequality.

    theorem row_minus_lt_iff {h i : ℕ} {child parent : VariablePosition h}
    (hc : AtLevel (i + 1) false child) (hp : AtLevel i false parent) :
    TreePositions.rowKey h parent < TreePositions.rowKey h child ↔
      node parent ≤ node child / 2 := by
…

    Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.TreePositions.rowKey, OAI.Problem348.Construction.node

  6. theorem OAI.Problem348.Construction.column_plus_lt_iff line 74

    Source documentation

    Column plus parent precedes column plus child exactly for the parent-node inequality.

    theorem column_plus_lt_iff {h i : ℕ} {child parent : VariablePosition h}
    (hc : AtLevel (i + 1) true child) (hp : AtLevel i true parent) :
    TreePositions.columnKey h parent < TreePositions.columnKey h child ↔
      node parent ≤ node child / 2 := by
…

    Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.TreePositions.columnKey, OAI.Problem348.Construction.node

  7. theorem OAI.Problem348.Construction.column_minus_lt_iff line 85

    Source documentation

    Column minus child precedes column minus parent exactly for the parent-node inequality.

    theorem column_minus_lt_iff {h i : ℕ} {child parent : VariablePosition h}
    (hc : AtLevel (i + 1) false child) (hp : AtLevel i false parent) :
    TreePositions.columnKey h child < TreePositions.columnKey h parent ↔
      node child / 2 ≤ node parent := by
…

    Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.TreePositions.columnKey, OAI.Problem348.Construction.node