OAI/Computability/RandomMean/Growth.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.fold_digits line 35
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.solve_small line 46
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.foldMin line 54
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.foldMax line 58
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.smallVector line 64
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.nth line 80
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.scalar_bound line 88
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.column_bound line 92
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.coordinates_small line 100
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.RawMedian.boxed_small line 109
  11. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.Small line 119
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.positives_length line 120
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.negatives_length line 126
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.trueComplement_small line 132
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.falseComplement_small line 137
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.base_small line 142
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.extend_small line 157
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.combine_small line 166