OAI/LinearAlgebra/MatrixFields/Parameters/TerminalPopulations.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.law line 21
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.denominator line 23
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.dilation line 26
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count line 28
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.denominator_pos line 33
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.dilation_pos line 36
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.baseCount_cast line 39
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.sum_baseCount line 45
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.population_dilation line 51
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.populationLength_dilation line 58
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.sum_count line 65
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_cast line 73
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_cast_real line 83
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_dilate line 91
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_mul_one line 98
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.source_population_pos line 103
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.sum_count_pos line 109
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_positive_law_positive line 117
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_pos_iff line 129
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_eq_zero_of_law_eq_zero line 143
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_ratio line 150
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.count_ratio_real line 164
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.normalizedCountLaw_mass line 174
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalPopulations.normalizedCountLaw_mass_eq line 182