OAI/Computability/PerfectCompleteness/Algebra/BilinearWitnessLemmas.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BilinearWitness.assemble line 19
  2. theorem OAI.PerfectCompleteness.BilinearWitness.exists_child_pair line 23
  3. def OAI.PerfectCompleteness.BilinearWitness.Witness line 36
  4. def OAI.PerfectCompleteness.BilinearWitness.chooseWitness line 39
  5. def OAI.PerfectCompleteness.BilinearWitness.selected line 47
  6. theorem OAI.PerfectCompleteness.BilinearWitness.selected_card_le line 53
  7. theorem OAI.PerfectCompleteness.BilinearWitness.marked_of_restriction_zero line 62
  8. theorem OAI.PerfectCompleteness.BilinearProjection.disagreement_probability line 99
  9. theorem OAI.PerfectCompleteness.BilinearCollisionTransfer.probability_le_add_of_imp line 143
  10. abbrev OAI.PerfectCompleteness.BilinearCollisionTransfer.Form line 160
  11. def OAI.PerfectCompleteness.BilinearCollisionTransfer.fullCollision line 162
  12. def OAI.PerfectCompleteness.BilinearCollisionTransfer.restrictedCollision line 165
  13. theorem OAI.PerfectCompleteness.BilinearCollisionTransfer.collision_split line 170
  14. theorem OAI.PerfectCompleteness.BilinearCollisionTransfer.restricted_le_full_add line 184
  15. theorem OAI.PerfectCompleteness.BilinearCollisionTransfer.full_collision_transfer line 211