OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/NativeGroupedEntropy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure line 21
  2. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_total line 26
  3. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_zero_of_mass_zero line 39
  4. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.group_term_eq_homogeneous line 61
  5. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_eq_sum_homogeneous line 75
  6. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.homogeneousEntropy_mul_normalized line 83
  7. def OAI.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup line 95
  8. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup_eq_inl line 99
  9. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup_eq_inr line 112
  10. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_singleton line 118
  11. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_residual line 127
  12. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_singletons_residuals line 134
  13. abbrev OAI.MatrixMultiplication.JointNativeGroupedEntropy.SupportIndex line 160
  14. def OAI.MatrixMultiplication.JointNativeGroupedEntropy.ownWeight line 162
  15. def OAI.MatrixMultiplication.JointNativeGroupedEntropy.nativeGroup line 167
  16. theorem OAI.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_eq_native line 174