OAI/RepresentationTheory/UniversalSquare/Capacity/Capacity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Capacity.

  1. def OAI.UniversalTensorSquare.colPrefix line 18
  2. lemma OAI.UniversalTensorSquare.colPrefix_eq_sum line 20
  3. lemma OAI.UniversalTensorSquare.mem_colTruncate line 24
  4. lemma OAI.UniversalTensorSquare.rowTruncate_subset line 29
  5. lemma OAI.UniversalTensorSquare.colTruncate_subset line 34
  6. lemma OAI.UniversalTensorSquare.colTruncate_card line 39
  7. lemma OAI.UniversalTensorSquare.strip_area_identity line 43
  8. lemma OAI.UniversalTensorSquare.corner_subset_rectangle line 59
  9. lemma OAI.UniversalTensorSquare.prefix_last_mul_le line 73
  10. theorem OAI.UniversalTensorSquare.capacity_rectangle line 81
  11. def OAI.UniversalTensorSquare.bandCapacity line 151
  12. def OAI.UniversalTensorSquare.BandTest line 154
  13. lemma OAI.UniversalTensorSquare.capacity_floor_bound line 158
  14. lemma OAI.UniversalTensorSquare.prefix_le_capacity line 160
  15. lemma OAI.UniversalTensorSquare.capacity_large_numeric line 169
  16. theorem OAI.UniversalTensorSquare.capacity_large line 176