OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/PairWindows.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.base line 27
  2. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.q line 31
  3. abbrev OAI.MatrixMultiplication.AllFieldGroupPairWindows.Positions line 37
  4. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.pairCounts line 42
  5. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentBase line 49
  6. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentPair line 52
  7. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.classMass line 58
  8. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.windowFactor line 62
  9. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.windowFactor_pos line 65
  10. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentBase_pos line 70
  11. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.parent_positions_card line 74
  12. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.positions_card line 82
  13. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentPair_eq_parentCenter line 96
  14. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentPair_eq_native line 111
  15. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.parentStatistic line 125
  16. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.parent_window line 131
  17. def OAI.MatrixMultiplication.AllFieldGroupPairWindows.weightCode line 165
  18. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.weightCode_val line 171
  19. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.weightCode_statistic line 175
  20. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.left_supported_zero line 180
  21. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.filtered_pair_sum line 195
  22. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.q_eq_conditionalCenter line 233
  23. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.classMass_pos line 248
  24. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.fiber_mass line 254
  25. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.width_le line 267
  26. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.sharing_window line 290
  27. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.q_eq_one_of_subsingleton line 318
  28. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.pairWindow_of_completeKeep line 354
  29. theorem OAI.MatrixMultiplication.AllFieldGroupPairWindows.passing_pairWindow line 387