OAI/Computability/PerfectCompleteness/Decoding/UpperScalarPairAveraging.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.map_right line 21
  2. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.map_three line 31
  3. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.product_mixture line 41
  4. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.tapeLaw_cast line 64
  5. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.assocTapeEquiv_law line 74
  6. def OAI.PerfectCompleteness.UpperScalarPairAveraging.pathPairLaw line 84
  7. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.upper_step_tape_law line 96
  8. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.upper_read_law line 127
  9. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.fixed_pairLaw line 145
  10. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.continued_pairLaw_eq_mixture line 186
  11. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.geometric_tagLaw line 205
  12. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.lower_geometric_pairLaw line 211
  13. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.upper_geometric_pairLaw line 227
  14. theorem OAI.PerfectCompleteness.UpperScalarPairAveraging.geometric_average_eq_actual line 242