OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ConstructionLabels.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldConstructionRates.denominator line 20
  2. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.denominator_pos line 22
  3. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.population_length line 25
  4. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.populationLength_tendsto line 29
  5. abbrev OAI.MatrixMultiplication.AllFieldConstructionRates.Slot line 37
  6. def OAI.MatrixMultiplication.AllFieldConstructionRates.capacity line 39
  7. def OAI.MatrixMultiplication.AllFieldConstructionRates.selectionRate line 44
  8. def OAI.MatrixMultiplication.AllFieldConstructionRates.initialCount line 47
  9. def OAI.MatrixMultiplication.AllFieldConstructionRates.groupCount line 50
  10. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.initialCount_eq line 54
  11. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.groupCount_eq_native line 59
  12. abbrev OAI.MatrixMultiplication.AllFieldConstructionRates.SelectedLabels line 71
  13. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_selected line 75
  14. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_selected_product line 81
  15. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_selected_from_factors line 87
  16. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.slot_card line 97
  17. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.sum_capacity line 101
  18. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.sum_selectionRate line 111
  19. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.selected_pos line 119
  20. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.selected_rate line 127
  21. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.exists_positive_slack line 156
  22. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.exists_slack_for_loss line 170
  23. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.capacity_pos_of_native line 197
  24. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.eventually_capacity_pos line 209
  25. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.terminalDilation_mul_one line 223
  26. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.terminalDilation_tendsto line 229
  27. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.terminal_denominator line 240
  28. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.selected_terminal_rate line 245
  29. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.selected_terminal_rate_of_cardinality line 256