OAI/Computability/PerfectCompleteness/Sampling/WholeArrayHiddenLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.product_assoc_pushforward line 18
  2. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.product_split_first line 29
  3. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.product_read_second line 52
  4. abbrev OAI.PerfectCompleteness.WholeArrayHiddenLaw.RestIndex line 62
  5. abbrev OAI.PerfectCompleteness.WholeArrayHiddenLaw.Factor line 65
  6. instance OAI.PerfectCompleteness.WholeArrayHiddenLaw.factorFintype line 71
  7. abbrev OAI.PerfectCompleteness.WholeArrayHiddenLaw.RestTape line 77
  8. instance OAI.PerfectCompleteness.WholeArrayHiddenLaw.restFactorFintype line 81
  9. instance OAI.PerfectCompleteness.WholeArrayHiddenLaw.restTapeFintype line 87
  10. abbrev OAI.PerfectCompleteness.WholeArrayHiddenLaw.ScalarTape line 96
  11. instance OAI.PerfectCompleteness.WholeArrayHiddenLaw.scalarTapeFintype line 100
  12. def OAI.PerfectCompleteness.WholeArrayHiddenLaw.scalarLaw line 111
  13. def OAI.PerfectCompleteness.WholeArrayHiddenLaw.restLaw line 116
  14. def OAI.PerfectCompleteness.WholeArrayHiddenLaw.splitRoot line 125
  15. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.splitRoot_law line 131
  16. def OAI.PerfectCompleteness.WholeArrayHiddenLaw.split line 145
  17. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.split_law line 155
  18. theorem OAI.PerfectCompleteness.WholeArrayHiddenLaw.split_readout_law line 181