OAI/LinearAlgebra/MatrixFields/Entropy/TerminalRates.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts line 23
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalDilation line 26
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalLength line 29
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalDilation_pos line 32
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalLength_pos line 36
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalLength_mul_one line 40
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_pos line 45
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_ratio line 50
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum_inl line 56
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum_inr line 61
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum line 66
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_repeat line 71
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_repeat_sum line 77
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.statisticCounts_sum_cast line 84
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.ZeroWords line 90
  16. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroWordsFintype line 98
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_inl line 102
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_inr line 107
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroWords_card_pos line 112
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroWords_local line 133
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroWords line 158
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroVolume line 178
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.zeroVolume_pos line 181
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.log_zeroVolume line 186
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.tendsto_zeroVolume line 193
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalVolume line 208
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.stageCVolume_pos line 213
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.terminalVolume_pos line 219
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.log_terminalVolume line 225
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.normalized_log_initialVolume line 243
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.normalized_log_stageCVolume line 255
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.tendsto_terminalVolume line 263