OAI/NumberTheory/Ostmann/Tree/QuartetHeld.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Tree.Quartet.NodeInput.actual_held_square_left line 12
  2. theorem OAI.Ostmann.Tree.Quartet.NodeInput.actual_held_square_right line 18
  3. theorem OAI.Ostmann.Tree.Quartet.NodeInput.residual_held_ratio line 24
  4. theorem OAI.Ostmann.Tree.Quartet.NodeInput.shared_held_ratio line 34
  5. def OAI.Ostmann.Tree.Quartet.NodeInput.leftNode line 44
  6. def OAI.Ostmann.Tree.Quartet.NodeInput.rightNode line 49
  7. theorem OAI.Ostmann.Tree.Quartet.NodeInput.leftNode_argument line 54
  8. theorem OAI.Ostmann.Tree.Quartet.NodeInput.rightNode_argument line 63
  9. theorem OAI.Ostmann.Tree.Quartet.NodeInput.leftNode_shared line 72
  10. theorem OAI.Ostmann.Tree.Quartet.NodeInput.rightNode_shared line 76
  11. theorem OAI.Ostmann.Tree.Quartet.NodeInput.left_bad_ratio line 80
  12. theorem OAI.Ostmann.Tree.Quartet.NodeInput.right_bad_ratio line 93