OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/APFree.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointAPFree.natSet line 13
  2. theorem OAI.MatrixMultiplication.JointAPFree.natSet_subset line 15
  3. theorem OAI.MatrixMultiplication.JointAPFree.natSet_card line 18
  4. theorem OAI.MatrixMultiplication.JointAPFree.natSet_threeAPFree line 21
  5. theorem OAI.MatrixMultiplication.JointAPFree.mem_natSet_lt line 24
  6. theorem OAI.MatrixMultiplication.JointAPFree.natCast_injective_below line 27
  7. theorem OAI.MatrixMultiplication.JointAPFree.add_lt_modulus line 32
  8. def OAI.MatrixMultiplication.JointAPFree.modularSet line 37
  9. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_card line 40
  10. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_threeAPFree line 48
  11. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_hashAP line 63
  12. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_card_lower line 71
  13. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_card_le_half line 77
  14. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_card_pos line 81
  15. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_nonempty line 88
  16. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_log_card_lower line 91
  17. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_log_card_le_half line 100
  18. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_log_card_lower_modulus line 106
  19. theorem OAI.MatrixMultiplication.JointAPFree.modularSet_log_card_le_modulus line 125