OAI/Computability/PerfectCompleteness/Sampling/CutSamplerKeyLocalityLemmas.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CutSamplerKeyLocality.F2 line 15
  2. def OAI.PerfectCompleteness.CutSamplerKeyLocality.keptLeaf line 23
  3. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.view_eq_of_keptLeaf line 28
  4. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.keptLeaf_at_cut line 52
  5. def OAI.PerfectCompleteness.CutSamplerKeyLocality.numberedKeep line 66
  6. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.not_numberedKeep_clean line 70
  7. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.view_eq_of_numbered_retained line 80
  8. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.view_eq_of_retained line 99
  9. def OAI.PerfectCompleteness.CutSamplerKeyLocality.rowQuery line 115
  10. def OAI.PerfectCompleteness.CutSamplerKeyLocality.numberedRows line 118
  11. def OAI.PerfectCompleteness.CutSamplerKeyLocality.allRowsZero line 121
  12. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.numberedRows_constant line 124
  13. def OAI.PerfectCompleteness.CutSamplerKeyLocality.retainedRows line 133
  14. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.retainedRows_eq_of_extension line 138
  15. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.numberedRows_factor line 147
  16. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.clean_position_dropped line 153
  17. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.key_eq_retained line 162
  18. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.label_eq_retained line 172
  19. theorem OAI.PerfectCompleteness.CutSamplerKeyLocality.response_eq_retained line 184
  20. def OAI.PerfectCompleteness.CutSamplerReplay.Tape line 213
  21. def OAI.PerfectCompleteness.CutSamplerReplay.erase line 223
  22. def OAI.PerfectCompleteness.CutSamplerReplay.evaluate line 232
  23. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluate_refl line 243
  24. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluate_step line 249
  25. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluate_erase line 260
  26. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluate_erase_of_split_zero line 314
  27. abbrev OAI.PerfectCompleteness.CutSamplerReplayGrouping.RetainedTerminal line 341
  28. def OAI.PerfectCompleteness.CutSamplerReplayGrouping.exteriorStepIndex line 347
  29. def OAI.PerfectCompleteness.CutSamplerReplayGrouping.subExterior line 353
  30. theorem OAI.PerfectCompleteness.CutSamplerReplayGrouping.subExterior_splitTape line 360
  31. def OAI.PerfectCompleteness.CutSamplerReplayGrouping.assemble line 372
  32. theorem OAI.PerfectCompleteness.CutSamplerReplayGrouping.assemble_splitTape line 384
  33. theorem OAI.PerfectCompleteness.CutSamplerReplayGrouping.evaluate_assemble_splitTape line 421