OAI/LinearAlgebra/MatrixFields/Construction/JointCompatibilityScaling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseSize line 26
  2. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseTotal line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseEntropy line 30
  4. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseGroupSize line 34
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseGroupedEntropy line 38
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.baseSize_le_baseTotal line 43
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.sum_baseGroupSize line 48
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.classEntropy_repeated line 62
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.groupPos_card_repeated line 75
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.groupedEntropy_repeated line 95
  11. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.typeErrorFactor line 106
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.typeErrorFactor_nonneg line 108
  13. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.classErrorCoefficient line 114
  14. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.groupErrorCoefficient line 117
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.classTypeError_le line 122
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.wordTypeError_le line 136
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.groupedTypeError_le line 149
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.tendsto_typeErrorFactor_div line 163
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityScaling.tendsto_mul_typeErrorFactor_div line 176