OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CompatibilityControls.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointCompatibilityControls.exists_pos_le_family line 19
  2. def OAI.MatrixMultiplication.JointCompatibilityControls.residualBase line 42
  3. def OAI.MatrixMultiplication.JointCompatibilityControls.designatedBase line 45
  4. def OAI.MatrixMultiplication.JointCompatibilityControls.totalCenterCount line 48
  5. def OAI.MatrixMultiplication.JointCompatibilityControls.residualCenter line 52
  6. theorem OAI.MatrixMultiplication.JointCompatibilityControls.residualBase_mul_center line 59
  7. theorem OAI.MatrixMultiplication.JointCompatibilityControls.residualCenter_nonneg line 76
  8. theorem OAI.MatrixMultiplication.JointCompatibilityControls.residualCenter_le_one line 85
  9. def OAI.MatrixMultiplication.JointCompatibilityControls.groupCenter line 99
  10. def OAI.MatrixMultiplication.JointCompatibilityControls.groupCap line 105
  11. theorem OAI.MatrixMultiplication.JointCompatibilityControls.groupCap_nonneg line 111
  12. theorem OAI.MatrixMultiplication.JointCompatibilityControls.exists_group_entropy_window line 126
  13. theorem OAI.MatrixMultiplication.JointCompatibilityControls.residual_card_repeated line 145
  14. theorem OAI.MatrixMultiplication.JointCompatibilityControls.repeated_mixture_balance line 159
  15. theorem OAI.MatrixMultiplication.JointCompatibilityControls.repeated_residual_width_le line 178
  16. theorem OAI.MatrixMultiplication.JointCompatibilityControls.exists_uniform_sideEntropyControl line 208
  17. def OAI.MatrixMultiplication.JointCompatibilityControls.control_mono_width line 261