OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CapacityAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointCapacityAlgebra.total_sub_max_degrees line 11
  2. theorem OAI.MatrixMultiplication.JointCapacityAlgebra.weighted_joint_capacity line 16