OAI/LinearAlgebra/MatrixFields/Entropy/GroupCountRate.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeLaw line 24
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeLaw_bounds line 29
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.weighted_classLaw_eq_native line 36
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.compatible_iff_native line 50
  5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeCount line 91
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.conditionalCount_eq_native line 100
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.competitors_card_le_nativeCount line 110
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.competitors_subset_eligibility_of_first line 118
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.eventually_eligibility_card_le line 132
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupDegreeLaws.eventually_first_competitors_card_le line 143
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.nativeCompatibilityRate line 182
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.base_positive_counts line 191
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.nativeLaw_normalized line 200
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.classCounts_dilation line 210
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.exists_widths_eventually_nativeCount_le line 222
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCountRate.exists_threshold_eventually_competitors_le line 284