OAI/Combinatorics/BalancedRyser/Candidates/CandidateRootFibers.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.TupleAlignment.RootPrescription.choice line 13
  2. theorem OAI.Balanced.TupleAlignment.RootPrescription.choice_tuple line 18
  3. theorem OAI.Balanced.TupleAlignment.RootPrescription.choice_direction line 23
  4. theorem OAI.Balanced.TupleAlignment.RootPrescription.tuple_injective line 28
  5. theorem OAI.Balanced.TupleAlignment.RootPrescription.choice_injective line 39
  6. def OAI.Balanced.TupleAlignment.RootPrescription.ofTuple line 44
  7. theorem OAI.Balanced.TupleAlignment.RootPrescription.ofTuple_tuple line 51
  8. def OAI.Balanced.TupleAlignment.successfulPrescriptions line 55
  9. theorem OAI.Balanced.TupleAlignment.successfulPrescriptions_card line 61
  10. theorem OAI.Balanced.TupleAlignment.choice_on_line_of_successful line 64
  11. def OAI.Balanced.TupleAlignment.successfulChoices line 72
  12. theorem OAI.Balanced.TupleAlignment.successfulChoices_card line 75
  13. def OAI.Balanced.TupleAlignment.validPrescriptions line 80
  14. theorem OAI.Balanced.TupleAlignment.exists_valid_prescription line 84
  15. theorem OAI.Balanced.TupleAlignment.supportsValidTuple_iff_valid_prescription line 105
  16. def OAI.Balanced.TupleAlignment.invalidSuccessCount line 120
  17. theorem OAI.Balanced.TupleAlignment.valid_add_invalid_eq_success line 123
  18. def OAI.Balanced.TupleAlignment.rootFiberSquareCount line 127
  19. def OAI.Balanced.TupleAlignment.commonLineSuccessPairs line 131
  20. theorem OAI.Balanced.TupleAlignment.rootFiberSquareCount_eq_pair_card line 136
  21. theorem OAI.Balanced.TupleAlignment.rootFiberSquareCount_eq_sum_fibers line 154
  22. theorem OAI.Balanced.TupleAlignment.mem_successfulPrescriptions_fiber_iff line 168
  23. theorem OAI.Balanced.TupleAlignment.mem_commonLineSuccessPairs_iff line 184
  24. theorem OAI.Balanced.TupleAlignment.mean_rootFiberSquareCount line 207
  25. theorem OAI.Balanced.TupleAlignment.successfulChoices_fiber_card line 241
  26. theorem OAI.Balanced.TupleAlignment.successfulChoices_square_sum line 247
  27. theorem OAI.Balanced.TupleAlignment.candidateSlot_lower_bound_of_root_counts line 254