OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/TerminalPopulations.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldTerminalPopulations.law line 19
  2. def OAI.MatrixMultiplication.AllFieldTerminalPopulations.denominator line 21
  3. def OAI.MatrixMultiplication.AllFieldTerminalPopulations.dilation line 24
  4. def OAI.MatrixMultiplication.AllFieldTerminalPopulations.count line 26
  5. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.denominator_pos line 31
  6. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.dilation_pos line 34
  7. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.baseCount_cast line 37
  8. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.sum_baseCount line 43
  9. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.population_dilation line 49
  10. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.populationLength_dilation line 56
  11. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.sum_count line 63
  12. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_cast line 71
  13. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_cast_real line 81
  14. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_dilate line 89
  15. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_mul_one line 96
  16. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.source_population_pos line 101
  17. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.sum_count_pos line 107
  18. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_positive_law_positive line 115
  19. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_pos_iff line 127
  20. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_eq_zero_of_law_eq_zero line 141
  21. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_ratio line 148
  22. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.count_ratio_real line 162
  23. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.normalizedCountLaw_mass line 172
  24. theorem OAI.MatrixMultiplication.AllFieldTerminalPopulations.normalizedCountLaw_mass_eq line 180