OAI/RepresentationTheory/UniversalSquare/Capacity/RegionExhaustion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Region Exhaustion.

  1. def OAI.UniversalTensorSquare.semanticResidualCheck line 15
  2. def OAI.UniversalTensorSquare.boundsEntail line 22
  3. instance OAI.UniversalTensorSquare.(instance at line 25) line 25
  4. lemma OAI.UniversalTensorSquare.boundsEntail_sound line 28
  5. abbrev OAI.UniversalTensorSquare.PrefixRegion line 34
  6. def OAI.UniversalTensorSquare.regionCheck line 36
  7. instance OAI.UniversalTensorSquare.(instance at line 43) line 43
  8. lemma OAI.UniversalTensorSquare.regionCheck_sound line 47
  9. lemma OAI.UniversalTensorSquare.rowsWithin_of_checks line 61
  10. theorem OAI.UniversalTensorSquare.semantic_capacity_dichotomy line 69
  11. theorem OAI.UniversalTensorSquare.candidate_semantic_pos line 120