OAI/LinearAlgebra/MatrixFields/Extraction/ConstructionLabels.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.denominator line 22
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.denominator_pos line 24
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.population_length line 27
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.populationLength_tendsto line 31
  5. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.Slot line 39
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.capacity line 41
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.selectionRate line 46
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.initialCount line 49
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.groupCount line 52
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.initialCount_eq line 56
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.groupCount_eq_native line 61
  12. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.SelectedLabels line 73
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_selected line 77
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_selected_product line 83
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.card_selected_from_factors line 89
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.slot_card line 99
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.sum_capacity line 103
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.sum_selectionRate line 113
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.selected_pos line 121
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.selected_rate line 129
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.exists_positive_slack line 158
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.exists_slack_for_loss line 172
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.capacity_pos_of_native line 199
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.eventually_capacity_pos line 211
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.terminalDilation_mul_one line 225
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.terminalDilation_tendsto line 231
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.terminal_denominator line 242
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.selected_terminal_rate line 247
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionRates.selected_terminal_rate_of_cardinality line 258