OAI/LinearAlgebra/MatrixFields/Construction/JointCompatibilityCountProducer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.exists_pos_le_family_inline_MatrixMultiplication_JointCompatibilityCountProducer line 21
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.exists_group_entropy_window_inline_MatrixMultiplication_JointCompatibilityCountProducer line 45
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.repeated_residual_width_le_inline_MatrixMultiplication_JointCompatibilityCountProducer line 64
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.exists_uniform_sideEntropyControl_all_positions line 94
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.aggregateCoefficient line 152
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.aggregate_error_of_pairWindow line 157
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityCountProducer.exists_widths_eventually_count_le line 241