OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CompatibilityScaling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointCompatibilityScaling.baseSize line 22
  2. def OAI.MatrixMultiplication.JointCompatibilityScaling.baseTotal line 24
  3. def OAI.MatrixMultiplication.JointCompatibilityScaling.baseEntropy line 26
  4. def OAI.MatrixMultiplication.JointCompatibilityScaling.baseGroupSize line 30
  5. def OAI.MatrixMultiplication.JointCompatibilityScaling.baseGroupedEntropy line 34
  6. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.baseSize_le_baseTotal line 39
  7. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.sum_baseGroupSize line 44
  8. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.classEntropy_repeated line 58
  9. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.groupPos_card_repeated line 71
  10. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.groupedEntropy_repeated line 91
  11. def OAI.MatrixMultiplication.JointCompatibilityScaling.typeErrorFactor line 102
  12. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.typeErrorFactor_nonneg line 104
  13. def OAI.MatrixMultiplication.JointCompatibilityScaling.classErrorCoefficient line 110
  14. def OAI.MatrixMultiplication.JointCompatibilityScaling.groupErrorCoefficient line 113
  15. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.classTypeError_le line 118
  16. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.wordTypeError_le line 131
  17. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.groupedTypeError_le line 144
  18. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.tendsto_typeErrorFactor_div line 158
  19. theorem OAI.MatrixMultiplication.JointCompatibilityScaling.tendsto_mul_typeErrorFactor_div line 171