OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialLeafRates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldInitialLeafRates.InitialZero line 19
  2. abbrev OAI.MatrixMultiplication.AllFieldInitialLeafRates.PopulationHistory line 22
  3. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.shapeMax_lt line 24
  4. def OAI.MatrixMultiplication.AllFieldInitialLeafRates.shapeIndex line 29
  5. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.card_alphabet line 32
  6. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.card_alphabet_pos line 39
  7. abbrev OAI.MatrixMultiplication.AllFieldInitialLeafRates.Words line 45
  8. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.card_words line 50
  9. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.card_words_pos line 57
  10. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.log_card_words line 63
  11. abbrev OAI.MatrixMultiplication.AllFieldInitialLeafRates.ProductWords line 70
  12. def OAI.MatrixMultiplication.AllFieldInitialLeafRates.volume line 73
  13. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.volume_eq_prod line 76
  14. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.volume_pos line 81
  15. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.log_volume line 86
  16. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.sum_populationHistory_rate line 106
  17. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.log_volume_eq_S0 line 122
  18. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.normalized_log_volume_eq_S0 line 127
  19. theorem OAI.MatrixMultiplication.AllFieldInitialLeafRates.tendsto_normalized_log_volume line 137