OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/ProjectedGroupEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.groupMass_designated_some line 24
  2. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.weighted_groupLaw_designated_some line 29
  3. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.groupedEntropy_counts_eq_total_mul line 45
  4. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.baseGroupSize_eq_groupMass line 76
  5. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.residualCenter_eq_groupLaw line 98
  6. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.projectedReferenceEntropy_eq_sum_counts_groupedEntropy line 114
  7. theorem OAI.MatrixMultiplication.JointProjectedGroupEntropy.projectedReferenceEntropy_eq_sum_weighted_groupedEntropy line 136