OAI/Computability/MinUncut/Estimates/ListDecoding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Outer.paddedChoice line 12
  2. lemma OAI.MinUncut.Outer.paddedChoice_covers line 15
  3. structure OAI.MinUncut.Outer.HintLists line 25
  4. def OAI.MinUncut.Outer.HintLists.strategy line 29
  5. def OAI.MinUncut.Outer.HintLists.matches line 34
  6. lemma OAI.MinUncut.Outer.HintLists.matching_le_sum line 40
  7. theorem OAI.MinUncut.Outer.HintLists.shared_soundness line 64
  8. abbrev OAI.MinUncut.Outer.CoordinateSlot line 104
  9. abbrev OAI.MinUncut.Outer.FirstCoordinateSpace line 105
  10. def OAI.MinUncut.Outer.firstCoordinates line 107
  11. lemma OAI.MinUncut.Outer.firstCoordinates_apply line 113
  12. lemma OAI.MinUncut.Outer.firstCoordinates_symm_apply line 118
  13. def OAI.MinUncut.Outer.formsTransport line 121
  14. def OAI.MinUncut.Outer.firstFormCoordinates line 131
  15. lemma OAI.MinUncut.Outer.firstFormCoordinates_apply line 137
  16. abbrev OAI.MinUncut.Outer.TupleCoordinateData line 145
  17. def OAI.MinUncut.Outer.tupleCoordinateSlice line 149
  18. def OAI.MinUncut.Outer.tupleCoordinateGenerator line 155
  19. lemma OAI.MinUncut.Outer.tupleCoordinateGenerator_surjective line 159
  20. lemma OAI.MinUncut.Outer.uniform_tupleCoordinateGenerator line 167