OAI/LinearAlgebra/MatrixFields/Entropy/JointCompatibilityRateLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.exists_pos_le_family_inline_MatrixMultiplication_JointCompatibilityRateLimit line 21
  2. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.totalBase line 46
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.pairReferenceEntropy line 48
  4. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.projectedReferenceEntropy line 51
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityRate line 55
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.projectedReferenceEntropy_add_const line 63
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityRate_add_caps line 71
  8. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.PairWindow line 81
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.exists_pair_entropy_window line 88
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.repeated_positions_card line 104
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.repeated_positions_card_le line 113
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.pair_classEntropy_lower line 123
  13. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.errorCoefficient line 153
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.compatibilityExponent_le_rate_add line 160
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.exists_window_eventually_exponent_le line 195
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityRateLimit.exists_window_eventually_count_le line 231