OAI/LinearAlgebra/MatrixFields/Construction/JointMarginalSupport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.localWord line 23
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.localWord_injective line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.localAllowed line 39
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.localAllowed_of_mem_ambient line 44
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.sameSide line 51
  6. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.sharedAmbient line 54
  7. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.classBound line 59
  8. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.classExponent line 69
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.classBound_eq_exp line 80
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.classExponent_target_eq line 89
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.sharedAmbient_card_le line 95
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.sharesSide_iff line 130
  13. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.neighbors line 158
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.neighbors_card_le_sum line 162
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.neighbors_card_le line 178
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.neighbors_card_le_three_exp line 191
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientDegree.log_neighbors_card_le line 211
  18. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.Letter line 243
  19. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.Class line 246
  20. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.Symbol line 248
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.projectedStatistic line 251
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.classDesignated line 255
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.classLaw line 259
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.tripleSide_eq_sideWord line 263
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.tripleSide_triple line 269
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.childWidth_le line 276
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.fineCompatible_uniform line 286
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.uniformCompatible line 304
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.Compatible_uniform line 315
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.conditionalCount line 332
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.uniformCompatible_count line 341
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.competitors_card_le_conditionalCount line 353
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegrees.eligibility_card_le_sharedAmbient line 378
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMarginalSupport.localAllowed_coordinate_witness line 422
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMarginalSupport.localAllowed_coordinate_support line 434
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMarginalSupport.localAllowed_parent_bounds line 445
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointMarginalSupport.localAllowed_positive_reference line 453