OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CompatibilityIncidence.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointCompatibilityIncidence.ClassPerm line 24
  2. def OAI.MatrixMultiplication.JointCompatibilityIncidence.permuteFixedWords line 26
  3. def OAI.MatrixMultiplication.JointCompatibilityIncidence.fixedWordsMulAction line 33
  4. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.fixedWordsPretransitive line 52
  5. def OAI.MatrixMultiplication.JointCompatibilityIncidence.jointCount line 72
  6. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.jointCount_reindex line 75
  7. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.jointCount_sum_shapes line 83
  8. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.projected_restrict_population line 95
  9. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.residual_population_add_designated line 114
  10. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.projected_population_fixed line 131
  11. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.residual_projected_window line 145
  12. def OAI.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup line 186
  13. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_eq_some line 190
  14. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_eq_none line 202
  15. abbrev OAI.MatrixMultiplication.JointCompatibilityIncidence.GroupPos line 206
  16. def OAI.MatrixMultiplication.JointCompatibilityIncidence.groupProjection line 209
  17. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupPos_card_some line 214
  18. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupPos_card_none line 220
  19. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.restrict_card_eq_sum_population line 226
  20. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupProjection_population_some line 234
  21. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupProjection_population_none line 245
  22. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.normalized_count_window line 253
  23. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.group_entropy_of_designated_windows line 263
  24. def OAI.MatrixMultiplication.JointCompatibilityIncidence.groupMass line 312
  25. def OAI.MatrixMultiplication.JointCompatibilityIncidence.groupLaw line 315
  26. def OAI.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy line 319
  27. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupMass_relabel line 323
  28. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupLaw_relabel line 329
  29. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_relabel line 335
  30. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupMass_reindex line 347
  31. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupLaw_reindex line 361
  32. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_reindex line 377
  33. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.groupedEntropy_add_reindex line 383
  34. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designatedGroup_transport line 391
  35. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designated_groupedEntropy_reindex line 397
  36. structure OAI.MatrixMultiplication.JointCompatibilityIncidence.SideEntropyControl line 425
  37. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.SideEntropyControl.group_entropy line 447
  38. def OAI.MatrixMultiplication.JointCompatibilityIncidence.DesignatedCompatibility line 488
  39. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designatedCompatibility_permute line 500
  40. def OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount line 511
  41. def OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount line 516
  42. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designated_incidence_count line 522
  43. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.designated_incidence_multinomial line 538
  44. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount_eq line 555
  45. def OAI.MatrixMultiplication.JointCompatibilityIncidence.wordEntropyBound line 570
  46. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount_le_grouped_entropy line 575
  47. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleStatisticCount_le_of_controls line 641
  48. theorem OAI.MatrixMultiplication.JointCompatibilityIncidence.compatibleCandidateCount_le_of_controls line 665