OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/AmbientDegree.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointAmbientDegree.localWord line 20
  2. theorem OAI.MatrixMultiplication.JointAmbientDegree.localWord_injective line 25
  3. def OAI.MatrixMultiplication.JointAmbientDegree.localAllowed line 36
  4. theorem OAI.MatrixMultiplication.JointAmbientDegree.localAllowed_of_mem_ambient line 41
  5. def OAI.MatrixMultiplication.JointAmbientDegree.sameSide line 48
  6. def OAI.MatrixMultiplication.JointAmbientDegree.sharedAmbient line 51
  7. def OAI.MatrixMultiplication.JointAmbientDegree.classBound line 56
  8. def OAI.MatrixMultiplication.JointAmbientDegree.classExponent line 66
  9. theorem OAI.MatrixMultiplication.JointAmbientDegree.classBound_eq_exp line 77
  10. theorem OAI.MatrixMultiplication.JointAmbientDegree.classExponent_target_eq line 86
  11. theorem OAI.MatrixMultiplication.JointAmbientDegree.sharedAmbient_card_le line 92
  12. theorem OAI.MatrixMultiplication.JointAmbientDegree.sharesSide_iff line 127
  13. def OAI.MatrixMultiplication.JointAmbientDegree.neighbors line 155
  14. theorem OAI.MatrixMultiplication.JointAmbientDegree.neighbors_card_le_sum line 159
  15. theorem OAI.MatrixMultiplication.JointAmbientDegree.neighbors_card_le line 172
  16. theorem OAI.MatrixMultiplication.JointAmbientDegree.neighbors_card_le_three_exp line 185
  17. theorem OAI.MatrixMultiplication.JointAmbientDegree.log_neighbors_card_le line 205