OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/AmbientDegree.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. def OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.potential line 21
  2. def OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.logNormalizer line 29
  3. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.placedLaw_log line 37
  4. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.localAllowed_positive line 48
  5. def OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.orderTotal line 77
  6. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.canonicalLaw_mass_eq line 79
  7. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.localAllowed_entropy_le line 93
  8. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.tendsto_firstExponent line 115
  9. theorem OAI.MatrixMultiplication.AllFieldGroupAmbientDegree.eventually_sharedAmbient_first_card_le line 145