OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/TerminalRates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts line 22
  2. def OAI.MatrixMultiplication.AllFieldTerminalRates.terminalDilation line 25
  3. def OAI.MatrixMultiplication.AllFieldTerminalRates.terminalLength line 28
  4. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.terminalDilation_pos line 31
  5. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.terminalLength_pos line 35
  6. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.terminalLength_mul_one line 39
  7. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_pos line 44
  8. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_ratio line 49
  9. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum line 55
  10. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_repeat line 60
  11. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_repeat_sum line 66
  12. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum_cast line 73
  13. def OAI.MatrixMultiplication.AllFieldTerminalRates.ZeroWords line 79
  14. instance OAI.MatrixMultiplication.AllFieldTerminalRates.zeroWordsFintype line 87
  15. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_inl line 91
  16. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_inr line 97
  17. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_pos line 103
  18. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroWords_local line 119
  19. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroWords line 152
  20. def OAI.MatrixMultiplication.AllFieldTerminalRates.zeroVolume line 172
  21. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.zeroVolume_pos line 175
  22. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.log_zeroVolume line 180
  23. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroVolume line 188
  24. def OAI.MatrixMultiplication.AllFieldTerminalRates.terminalVolume line 203
  25. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.stageCVolume_pos line 208
  26. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.terminalVolume_pos line 214
  27. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.log_terminalVolume line 220
  28. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.normalized_log_initialVolume line 238
  29. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.normalized_log_stageCVolume line 250
  30. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.tendsto_terminalVolume line 258