OAI/Computability/DepthThree/HashAffine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.BinaryHash.OutsideData line 18
  2. def OAI.DepthThreeLowerBound.BinaryHash.coordinateCube line 20
  3. def OAI.DepthThreeLowerBound.BinaryHash.SupportedOn line 23
  4. def OAI.DepthThreeLowerBound.BinaryHash.coordinateCubeExtend line 26
  5. theorem OAI.DepthThreeLowerBound.BinaryHash.coordinateCubeExtend_mem line 30
  6. def OAI.DepthThreeLowerBound.BinaryHash.coordinateCubeEquiv line 35
  7. def OAI.DepthThreeLowerBound.BinaryHash.supportedDataEquiv line 49
  8. theorem OAI.DepthThreeLowerBound.BinaryHash.supportedOn_zero line 63
  9. theorem OAI.DepthThreeLowerBound.BinaryHash.supportedOn_sub_of_mem line 68
  10. theorem OAI.DepthThreeLowerBound.BinaryHash.add_mem_coordinateCube line 75
  11. theorem OAI.DepthThreeLowerBound.BinaryHash.not_injOn_coordinateCube_iff line 82
  12. theorem OAI.DepthThreeLowerBound.BinaryHash.not_injOn_coordinateCube_iff_of_outside line 103
  13. def OAI.DepthThreeLowerBound.BinaryHash.supportedVectors line 109
  14. theorem OAI.DepthThreeLowerBound.BinaryHash.mem_supportedVectors line 113
  15. theorem OAI.DepthThreeLowerBound.BinaryHash.supportedVectors_card line 118
  16. def OAI.DepthThreeLowerBound.BinaryHash.nonzeroSupportedVectors line 129
  17. theorem OAI.DepthThreeLowerBound.BinaryHash.mem_nonzeroSupportedVectors line 132
  18. theorem OAI.DepthThreeLowerBound.BinaryHash.nonzeroSupportedVectors_card line 137
  19. def OAI.DepthThreeLowerBound.BinaryHash.kernelSeeds line 143
  20. theorem OAI.DepthThreeLowerBound.BinaryHash.mem_kernelSeeds line 147
  21. theorem OAI.DepthThreeLowerBound.BinaryHash.kernelSeeds_card line 152
  22. def OAI.DepthThreeLowerBound.BinaryHash.badSeeds line 162
  23. theorem OAI.DepthThreeLowerBound.BinaryHash.mem_badSeeds line 166
  24. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_eq_biUnion line 172
  25. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_eq_of_outside line 181
  26. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_card_le line 185
  27. theorem OAI.DepthThreeLowerBound.BinaryHash.injOn_coordinateCube_empty line 200
  28. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_empty line 206
  29. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_card_eq_zero_of_card_eq_zero line 212
  30. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_zero_data line 218
  31. theorem OAI.DepthThreeLowerBound.BinaryHash.injOn_coordinateCube_zero_output_iff line 224
  32. theorem OAI.DepthThreeLowerBound.BinaryHash.badSeeds_zero_output line 253