OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/TargetRate.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.source_unit_pos line 18
  2. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.source_length_dilation line 22
  3. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_dilation line 27
  4. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_dilation_fun line 35
  5. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_sum line 41
  6. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_eq_population line 47
  7. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_dilation line 53
  8. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_cast_real line 61
  9. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_pos line 68
  10. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.base_empirical_eq line 74
  11. def OAI.MatrixMultiplication.AllFieldGroupTargetRate.groupEntropyRate line 82
  12. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.groupEntropyRate_nonneg line 87
  13. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.baseEntropy_eq_groupEntropyRate line 95
  14. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.target_card_pos line 103
  15. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.tendsto_log_target_card_div line 108
  16. theorem OAI.MatrixMultiplication.AllFieldGroupTargetRate.tendsto_log_targetSet_card_div line 124