OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/PairMixtureControls.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointPairMixtureControls.pairMixture line 23
  2. theorem OAI.MatrixMultiplication.JointPairMixtureControls.sum_first_fiber line 29
  3. theorem OAI.MatrixMultiplication.JointPairMixtureControls.sum_second_fiber line 39
  4. theorem OAI.MatrixMultiplication.JointPairMixtureControls.base_eq_zero_of_size_eq_zero line 49
  5. theorem OAI.MatrixMultiplication.JointPairMixtureControls.totalCenterCount_eq_zero_of_size_eq_zero line 56
  6. theorem OAI.MatrixMultiplication.JointPairMixtureControls.pairMixture_left_balance line 64
  7. theorem OAI.MatrixMultiplication.JointPairMixtureControls.pairMixture_right_balance line 89