OAI/ModelTheory/Choiceless/Gaussian.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CPTSeparation.Gaussian.Scalar line 7
  2. structure OAI.CPTSeparation.Gaussian.Row line 9
  3. def OAI.CPTSeparation.Gaussian.Row.satisfies line 15
  4. def OAI.CPTSeparation.Gaussian.Row.tail line 18
  5. def OAI.CPTSeparation.Gaussian.Row.reduce line 20
  6. lemma OAI.CPTSeparation.Gaussian.Row.satisfies_cons line 24
  7. lemma OAI.CPTSeparation.Gaussian.Row.tail_iff line 29
  8. lemma OAI.CPTSeparation.Gaussian.Row.pivot_solution line 34
  9. lemma OAI.CPTSeparation.Gaussian.Row.reduce_iff line 40
  10. def OAI.CPTSeparation.Gaussian.Solvable line 56
  11. def OAI.CPTSeparation.Gaussian.pivot line 58
  12. def OAI.CPTSeparation.Gaussian.solve line 61
  13. lemma OAI.CPTSeparation.Gaussian.pivot_some line 67
  14. lemma OAI.CPTSeparation.Gaussian.pivot_none line 71
  15. lemma OAI.CPTSeparation.Gaussian.solvable_tail line 75
  16. lemma OAI.CPTSeparation.Gaussian.solvable_reduce line 90
  17. theorem OAI.CPTSeparation.Gaussian.solve_correct line 107
  18. def OAI.CPTSeparation.Gaussian.Row.dense line 123
  19. lemma OAI.CPTSeparation.Gaussian.Row.dense_eq line 127
  20. def OAI.CPTSeparation.Gaussian.Row.reduceDense line 134
  21. lemma OAI.CPTSeparation.Gaussian.Row.reduceDense_eq line 139
  22. def OAI.CPTSeparation.Gaussian.metered line 147
  23. theorem OAI.CPTSeparation.Gaussian.metered_answer line 155
  24. theorem OAI.CPTSeparation.Gaussian.metered_bound line 165
  25. theorem OAI.CPTSeparation.Gaussian.metered_correct line 184
  26. def OAI.CPTSeparation.OrderedQuery.coefficient line 195
  27. def OAI.CPTSeparation.OrderedQuery.incident line 199
  28. def OAI.CPTSeparation.OrderedQuery.normalizationRow line 203
  29. def OAI.CPTSeparation.OrderedQuery.consistencyRow line 207
  30. def OAI.CPTSeparation.OrderedQuery.rows line 212
  31. def OAI.CPTSeparation.OrderedQuery.decideQuery line 216
  32. lemma OAI.CPTSeparation.OrderedQuery.sum_subtype line 219
  33. lemma OAI.CPTSeparation.OrderedQuery.coefficient_eq line 224
  34. lemma OAI.CPTSeparation.OrderedQuery.incident_eq line 232
  35. lemma OAI.CPTSeparation.OrderedQuery.row_zero line 242
  36. def OAI.CPTSeparation.OrderedQuery.left line 245
  37. def OAI.CPTSeparation.OrderedQuery.right line 247
  38. lemma OAI.CPTSeparation.OrderedQuery.normalization_satisfies line 249
  39. lemma OAI.CPTSeparation.OrderedQuery.consistency_satisfies line 266
  40. lemma OAI.CPTSeparation.OrderedQuery.norm_mem line 306
  41. lemma OAI.CPTSeparation.OrderedQuery.consistency_mem line 310
  42. theorem OAI.CPTSeparation.OrderedQuery.rows_solvable_iff line 314
  43. theorem OAI.CPTSeparation.OrderedQuery.decideQuery_correct line 344
  44. theorem OAI.CPTSeparation.OrderedQuery.rows_length line 351
  45. theorem OAI.CPTSeparation.OrderedQuery.elimination_operations line 354
  46. structure OAI.CPTSeparation.SerialGaussian.Row line 370
  47. def OAI.CPTSeparation.SerialGaussian.Row.decode line 375
  48. def OAI.CPTSeparation.SerialGaussian.Row.encode line 378
  49. def OAI.CPTSeparation.SerialGaussian.Row.head line 381
  50. def OAI.CPTSeparation.SerialGaussian.Row.tail line 383
  51. def OAI.CPTSeparation.SerialGaussian.Row.reduce line 386
  52. def OAI.CPTSeparation.SerialGaussian.pivot line 391
  53. def OAI.CPTSeparation.SerialGaussian.solve line 394
  54. theorem OAI.CPTSeparation.SerialGaussian.Row.decode_encode line 400
  55. theorem OAI.CPTSeparation.SerialGaussian.Row.head_decode line 404
  56. theorem OAI.CPTSeparation.SerialGaussian.Row.decode_tail line 410
  57. theorem OAI.CPTSeparation.SerialGaussian.Row.decode_reduce line 416
  58. theorem OAI.CPTSeparation.SerialGaussian.pivot_decode line 423
  59. theorem OAI.CPTSeparation.SerialGaussian.solve_decode line 430
  60. def OAI.CPTSeparation.SerialGaussian.payload line 439
  61. theorem OAI.CPTSeparation.SerialGaussian.payload_length line 442
  62. def OAI.CPTSeparation.SerialGaussian.queryRows line 452
  63. theorem OAI.CPTSeparation.SerialGaussian.queryRows_correct line 455
  64. theorem OAI.CPTSeparation.SerialGaussian.query_payload_size line 462
  65. theorem OAI.CPTSeparation.SerialGaussian.reduce_payload_size line 472
  66. theorem OAI.CPTSeparation.SerialGaussian.tail_payload_size line 478
  67. def OAI.CPTSeparation.OrderedQuery.symbolIndex line 488
  68. theorem OAI.CPTSeparation.OrderedQuery.indexSymbol_symbolIndex line 492
  69. theorem OAI.CPTSeparation.OrderedQuery.symbolIndex_indexSymbol line 501
  70. def OAI.CPTSeparation.OrderedQuery.symbolEquiv line 504
  71. def OAI.CPTSeparation.OrderedQuery.cellIndex line 509
  72. theorem OAI.CPTSeparation.OrderedQuery.cellValue_index line 512
  73. def OAI.CPTSeparation.OrderedQuery.tableDecode line 516
  74. theorem OAI.CPTSeparation.OrderedQuery.tableDecode_tableBits line 519
  75. abbrev OAI.CPTSeparation.OrderedQuery.Alphabet line 526
  76. def OAI.CPTSeparation.OrderedQuery.encode line 528
  77. def OAI.CPTSeparation.OrderedQuery.decode line 531
  78. theorem OAI.CPTSeparation.OrderedQuery.tableBits_length line 535
  79. theorem OAI.CPTSeparation.OrderedQuery.encode_size line 538
  80. theorem OAI.CPTSeparation.OrderedQuery.decode_encode line 544
  81. theorem OAI.CPTSeparation.OrderedQuery.encode_injective line 557
  82. theorem OAI.CPTSeparation.OrderedQuery.encode_length line 561
  83. def OAI.CPTSeparation.OrderedQuery.encoding line 564
  84. def OAI.CPTSeparation.OrderedQuery.answer line 567
  85. theorem OAI.CPTSeparation.OrderedQuery.answer_correct line 569