OAI/RepresentationTheory/UniversalSquare/Support/ConstrainedRows.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Constrained Rows.

  1. def OAI.UniversalTensorSquare.clippedSum line 13
  2. def OAI.UniversalTensorSquare.ListRowBounds line 15
  3. def OAI.UniversalTensorSquare.ListColBounds line 18
  4. def OAI.UniversalTensorSquare.clipBudget line 21
  5. def OAI.UniversalTensorSquare.rowBudget line 24
  6. def OAI.UniversalTensorSquare.rejectedRows line 27
  7. instance OAI.UniversalTensorSquare.(instance at line 33) line 33
  8. def OAI.UniversalTensorSquare.allowedRow line 36
  9. instance OAI.UniversalTensorSquare.(instance at line 39) line 39
  10. def OAI.UniversalTensorSquare.constrainedRows line 42
  11. lemma OAI.UniversalTensorSquare.list_sum_le_mul_length line 52
  12. lemma OAI.UniversalTensorSquare.clippedSum_length_le line 62
  13. lemma OAI.UniversalTensorSquare.clippedSum_proportion line 73
  14. lemma OAI.UniversalTensorSquare.cross_product_bound line 89
  15. lemma OAI.UniversalTensorSquare.rowSum_proportion line 99
  16. lemma OAI.UniversalTensorSquare.rejectedRows_false line 116
  17. lemma OAI.UniversalTensorSquare.allowedRow_cons line 142
  18. lemma OAI.UniversalTensorSquare.clipBudget_cons line 156
  19. lemma OAI.UniversalTensorSquare.rowBudget_cons line 164
  20. lemma OAI.UniversalTensorSquare.mem_constrainedRows line 177