OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CompatibilityRateLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.exists_pos_le_family line 19
  2. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.totalBase line 44
  3. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.pairReferenceEntropy line 46
  4. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.projectedReferenceEntropy line 49
  5. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityRate line 53
  6. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.projectedReferenceEntropy_add_const line 61
  7. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityRate_add_caps line 69
  8. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.PairWindow line 79
  9. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.exists_pair_entropy_window line 86
  10. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.repeated_positions_card line 102
  11. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.repeated_positions_card_le line 111
  12. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.pair_classEntropy_lower line 121
  13. def OAI.MatrixMultiplication.JointCompatibilityRateLimit.errorCoefficient line 151
  14. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityExponent_le_rate_add line 158
  15. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.exists_window_eventually_exponent_le line 193
  16. theorem OAI.MatrixMultiplication.JointCompatibilityRateLimit.exists_window_eventually_count_le line 229