OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/SquareCounts.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. theorem OAI.MatrixMultiplication.SquareCounts.colorBA line 20
  2. theorem OAI.MatrixMultiplication.SquareCounts.colorBC line 21
  3. theorem OAI.MatrixMultiplication.SquareCounts.colorAB line 22
  4. theorem OAI.MatrixMultiplication.SquareCounts.colorAC line 23
  5. theorem OAI.MatrixMultiplication.SquareCounts.colorCB line 24
  6. theorem OAI.MatrixMultiplication.SquareCounts.colorCA line 25
  7. def OAI.MatrixMultiplication.SquareCounts.baseLeaf line 29
  8. def OAI.MatrixMultiplication.SquareCounts.baseLeafEquiv line 35
  9. theorem OAI.MatrixMultiplication.SquareCounts.baseLeaf_color line 43
  10. def OAI.MatrixMultiplication.SquareCounts.initialCount line 49
  11. theorem OAI.MatrixMultiplication.SquareCounts.base_conditionalCount line 54
  12. def OAI.MatrixMultiplication.SquareCounts.counts line 70
  13. theorem OAI.MatrixMultiplication.SquareCounts.conditionalCount_script line 76
  14. def OAI.MatrixMultiplication.SquareCounts.stageOne line 85
  15. def OAI.MatrixMultiplication.SquareCounts.stageTwo line 86
  16. def OAI.MatrixMultiplication.SquareCounts.stageThree line 87
  17. def OAI.MatrixMultiplication.SquareCounts.stageFour line 88
  18. theorem OAI.MatrixMultiplication.SquareCounts.factors_at_every_stage line 90
  19. theorem OAI.MatrixMultiplication.SquareCounts.counts_after_three line 95
  20. theorem OAI.MatrixMultiplication.SquareCounts.counts_after_four line 100
  21. theorem OAI.MatrixMultiplication.SquareCounts.actual_counts_after_three line 106
  22. theorem OAI.MatrixMultiplication.SquareCounts.actual_counts_after_four line 112
  23. def OAI.MatrixMultiplication.SquareCounts.completed line 118
  24. theorem OAI.MatrixMultiplication.SquareCounts.completion_unit_coefficients line 120
  25. theorem OAI.MatrixMultiplication.SquareCounts.script_unit_coefficients line 133
  26. def OAI.MatrixMultiplication.SquareCounts.tensor line 146
  27. theorem OAI.MatrixMultiplication.SquareCounts.tensor_unit_coefficients line 148
  28. abbrev OAI.MatrixMultiplication.SquareCounts.Leaf line 154
  29. def OAI.MatrixMultiplication.SquareCounts.retainedLeafEquiv line 156
  30. theorem OAI.MatrixMultiplication.SquareCounts.retainedLeafEquiv_coordinates line 160
  31. def OAI.MatrixMultiplication.SquareCounts.leafCount line 163
  32. theorem OAI.MatrixMultiplication.SquareCounts.leafCount_pos line 165
  33. theorem OAI.MatrixMultiplication.SquareCounts.card_termination_A line 167
  34. theorem OAI.MatrixMultiplication.SquareCounts.card_leaf line 178
  35. instance OAI.MatrixMultiplication.SquareCounts.leafNonempty line 182
  36. def OAI.MatrixMultiplication.SquareCounts.uniformLaw line 185
  37. theorem OAI.MatrixMultiplication.SquareCounts.uniformLaw_mass line 187
  38. theorem OAI.MatrixMultiplication.SquareCounts.uniformLaw_pos line 190
  39. theorem OAI.MatrixMultiplication.SquareCounts.uniformLaw_entropy line 194
  40. def OAI.MatrixMultiplication.SquareCounts.leafMultiplicity line 197
  41. theorem OAI.MatrixMultiplication.SquareCounts.totalMultiplicity line 199
  42. theorem OAI.MatrixMultiplication.SquareCounts.totalMultiplicity_pos line 202
  43. theorem OAI.MatrixMultiplication.SquareCounts.uniformLaw_mass_counts line 206
  44. def OAI.MatrixMultiplication.SquareCounts.retainedUniformLaw line 212
  45. theorem OAI.MatrixMultiplication.SquareCounts.retainedUniformLaw_mass line 215
  46. theorem OAI.MatrixMultiplication.SquareCounts.retainedUniformLaw_entropy line 221
  47. theorem OAI.MatrixMultiplication.SquareCounts.uniform_pairRate_sum line 226
  48. def OAI.MatrixMultiplication.SquareCounts.approximation line 237
  49. theorem OAI.MatrixMultiplication.SquareCounts.rank_power line 243