OAI/Computability/WeisfeilerLeman/Diagonal.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.Diagonal.unary_length line 6
  2. theorem OAI.WLTime.Diagonal.entryBits_length line 7
  3. theorem OAI.WLTime.Diagonal.tableBits_length_upper line 9
  4. theorem OAI.WLTime.Diagonal.tableBits_length_lower line 20
  5. theorem OAI.WLTime.Diagonal.designation_length line 27
  6. theorem OAI.WLTime.Diagonal.designation_bounds line 31
  7. theorem OAI.WLTime.Diagonal.designation_upper line 39
  8. theorem OAI.WLTime.Universal.stepBound_small line 53
  9. theorem OAI.WLTime.Universal.timeBound_small line 60
  10. theorem OAI.WLTime.Diagonal.pointwise_contradiction line 84
  11. theorem OAI.WLTime.Diagonal.padded_designation line 90
  12. theorem OAI.WLTime.Numeric.polylog_sublinear line 106
  13. def OAI.WLTime.Numeric.base line 137
  14. theorem OAI.WLTime.Numeric.base_lower line 138
  15. theorem OAI.WLTime.Numeric.base_upper line 144
  16. def OAI.WLTime.Numeric.chooseOrder line 155
  17. theorem OAI.WLTime.Numeric.chooseOrder_bounds line 156
  18. theorem OAI.WLTime.Numeric.order_polynomial line 168
  19. theorem OAI.WLTime.Numeric.pow_mono line 185
  20. theorem OAI.WLTime.Numeric.grow_one line 186
  21. theorem OAI.WLTime.Numeric.space_arith line 187
  22. theorem OAI.WLTime.Numeric.digits_le line 188
  23. theorem OAI.WLTime.Numeric.digits_polynomial line 191
  24. theorem OAI.WLTime.Numeric.sum_le_pow line 199
  25. theorem OAI.WLTime.Numeric.input_small line 203
  26. theorem OAI.WLTime.Numeric.scale6 line 212
  27. theorem OAI.WLTime.Numeric.consumer_inside line 214
  28. theorem OAI.WLTime.Numeric.writer_small line 216
  29. theorem OAI.WLTime.Numeric.consumer_small line 257
  30. theorem OAI.WLTime.OneTape.Symbolic.coefficient_pos line 284
  31. theorem OAI.WLTime.worstTime_ge line 294
  32. theorem OAI.WLTime.promised_pair line 300
  33. theorem OAI.WLTime.designation_small line 306
  34. theorem OAI.WLTime.time_window line 330
  35. theorem OAI.WLTime.space_window line 339
  36. def OAI.WLTime.conventionShift line 353
  37. theorem OAI.WLTime.pair_correct_convention line 354
  38. theorem OAI.WLTime.tm_pointwise line 364