OAI/LinearAlgebra/MatrixFields/Construction/JointCompatibilityIncidence.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.ClassPerm line 27
  2. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.permuteFixedWords line 29
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.fixedWordsMulAction line 36
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.fixedWordsPretransitive line 56
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.jointCount line 77
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.jointCount_reindex line 80
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.jointCount_sum_shapes line 88
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.projected_restrict_population line 100
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.residual_population_add_designated line 119
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.projected_population_fixed line 136
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.residual_projected_window line 150
  12. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup line 191
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_eq_some line 195
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_eq_none line 207
  15. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.GroupPos line 211
  16. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupProjection line 214
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupPos_card_some line 219
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupPos_card_none line 225
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.restrict_card_eq_sum_population line 231
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupProjection_population_some line 239
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupProjection_population_none line 250
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.normalized_count_window line 258
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.group_entropy_of_designated_windows line 268
  24. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupMass line 317
  25. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupLaw line 320
  26. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy line 324
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupMass_relabel line 328
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupLaw_relabel line 334
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_relabel line 340
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupMass_reindex line 352
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupLaw_reindex line 366
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_reindex line 382
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_add_reindex line 388
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_transport line 396
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designated_groupedEntropy_reindex line 402
  36. structure OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.SideEntropyControl line 430
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.SideEntropyControl.group_entropy line 452
  38. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.DesignatedCompatibility line 493
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designatedCompatibility_permute line 505
  40. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount line 516
  41. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount line 521
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designated_incidence_count line 527
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.designated_incidence_multinomial line 543
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount_eq line 560
  45. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.wordEntropyBound line 575
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount_le_grouped_entropy line 580
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount_le_of_controls line 646
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount_le_of_controls line 670