OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CompatibilityCountProducer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.exists_pos_le_family line 18
  2. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.exists_group_entropy_window line 42
  3. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.repeated_residual_width_le line 61
  4. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.exists_uniform_sideEntropyControl_all_positions line 91
  5. def OAI.MatrixMultiplication.JointCompatibilityCountProducer.aggregateCoefficient line 149
  6. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.aggregate_error_of_pairWindow line 154
  7. theorem OAI.MatrixMultiplication.JointCompatibilityCountProducer.exists_widths_eventually_count_le line 238