OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/ProjectedEntropy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_congr_law_on_support line 31
  2. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_designated_pushforward line 45
  3. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_const_one line 60
  4. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.pushforwardWeight_mask line 75
  5. def OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.maskedBranchMass line 96
  6. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.classCounts_cast_eq_pushforward line 101
  7. def OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchHalfLaw line 149
  8. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.class_groupedEntropy_eq_masked line 153
  9. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.maskedBranchMass_eq_conditional line 173
  10. def OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost line 184
  11. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.history_projected_entropy_eq line 194
  12. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost_eq line 208
  13. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost_eq_observed line 282
  14. theorem OAI.MatrixMultiplication.AllFieldGroupProjectedEntropy.projected_native_entropy_eq line 302