OAI/Combinatorics/MatrixRemoval/SampledPathOrder.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The four sampled body orders, including the shared-leaf edge.

  1. theorem OAI.Problem348.HostSampledPath.sample_plus_eq line 13
  2. theorem OAI.Problem348.HostSampledPath.sample_minus_eq line 21
  3. theorem OAI.Problem348.HostSampledPath.treeNode_mixFin line 25
  4. theorem OAI.Problem348.HostSampledPath.row_plus_sample_child_lt_parent line 29
  5. theorem OAI.Problem348.HostSampledPath.row_minus_sample_parent_lt_child line 38
  6. theorem OAI.Problem348.HostSampledPath.column_plus_sample_parent_lt_child line 47
  7. theorem OAI.Problem348.HostSampledPath.column_minus_sample_child_lt_parent line 56
  8. theorem OAI.Problem348.HostSampledPath.row_plus_sample_order line 66

    Source documentation

    Consequence after transporting the canonical row key into any ordered axis.

    theorem row_plus_sample_order {h : ℕ} {R : Type uR} [Preorder R]
    (r : Construction.Position h → R)
    (hr : ∀ p q : Construction.VariablePosition h,
      TreePositions.rowKey h p < TreePositions.rowKey h q →
        r (Sum.inr (Sum.inl p)) < r (Sum.inr (Sum.inl q)))
    (i : Fin h) (z u v : Fin (2 ^ h)) :
    r (position h (i.val + 1) (by omega) true z u) <
      r (position h i.val (by omega) true z v) :=
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.TreePositions.rowKey, OAI.Problem348.HostSampledPath.position

  9. theorem OAI.Problem348.HostSampledPath.row_minus_sample_order line 76
  10. theorem OAI.Problem348.HostSampledPath.column_plus_sample_order line 86
  11. theorem OAI.Problem348.HostSampledPath.column_minus_sample_order line 96