OAI/Computability/RandomMean/Orientation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Code.stream line 13
  2. def OAI.MeanPayoff.TreeDevice.Certified.Counter.enumRow line 21
  3. def OAI.MeanPayoff.TreeDevice.Certified.Counter.enumLoop line 22
  4. def OAI.MeanPayoff.TreeDevice.Certified.Counter.enum line 31
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.canonical line 34
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.enumLoop_eq line 37
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.enum_eq line 49
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.enum_ofFn line 53
  9. def OAI.MeanPayoff.TreeDevice.Certified.VectorsRep line 60
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.VectorRep.length line 63
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.VectorRep.nth line 67
  12. def OAI.MeanPayoff.TreeDevice.Certified.RawMedian.scalar line 74
  13. def OAI.MeanPayoff.TreeDevice.Certified.RawMedian.entry line 75
  14. def OAI.MeanPayoff.TreeDevice.Certified.RawMedian.column line 76
  15. def OAI.MeanPayoff.TreeDevice.Certified.RawMedian.coordinates line 77
  16. def OAI.MeanPayoff.TreeDevice.Certified.RawMedian.boxed line 79
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.column_values line 83
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.coordinates_rep line 93
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.boxed_rep line 106
  20. def OAI.MeanPayoff.TreeDevice.Certified.Code.getD line 138
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.getD_eval line 140
  22. def OAI.MeanPayoff.TreeDevice.Certified.Array.scalarLT line 151
  23. def OAI.MeanPayoff.TreeDevice.Certified.Array.scalarLE line 152
  24. def OAI.MeanPayoff.TreeDevice.Certified.Array.belowScalar line 153
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.scalarTest_rep line 155
  26. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.Data line 169
  27. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.Rep line 170
  28. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.ManyRep line 172
  29. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.positives line 175
  30. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.negatives line 178
  31. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.baseMask line 181
  32. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.singleton line 183
  33. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.trueComplement line 184
  34. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.falseComplement line 186
  35. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.baseOnMask line 188
  36. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.base line 190
  37. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.extend line 192
  38. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.combine line 194
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.positives_rep line 198
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.negatives_rep line 207
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.baseMask_rep line 218
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.base_rep line 234
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.extend_rep line 259
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.choices_length line 267
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.exceptions_rep line 276
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.combine_rep line 285