OAI/Computability/DirectedFeedback/Encoding/InstanceEquivalences.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Integration.InstanceEquivalences.renameConstraint line 12
  2. theorem OAI.DFVSGames.Integration.InstanceEquivalences.renameConstraint_satisfied line 18
  3. theorem OAI.DFVSGames.Integration.InstanceEquivalences.rename_count line 22
  4. def OAI.DFVSGames.Integration.InstanceEquivalences.renameInstance line 31
  5. theorem OAI.DFVSGames.Integration.InstanceEquivalences.countSatisfied_perm line 39
  6. theorem OAI.DFVSGames.Integration.InstanceEquivalences.satisfactionRate_eq_of_rename_perm line 46
  7. theorem OAI.DFVSGames.Integration.InstanceEquivalences.completeAt_iff_of_rename_perm line 58
  8. theorem OAI.DFVSGames.Integration.InstanceEquivalences.soundAt_iff_of_rename_perm line 72
  9. theorem OAI.DFVSGames.Integration.InstanceEquivalences.rename_rate line 86
  10. theorem OAI.DFVSGames.Integration.InstanceEquivalences.completeAt_rename_iff line 91
  11. theorem OAI.DFVSGames.Integration.InstanceEquivalences.soundAt_rename_iff line 96
  12. def OAI.DFVSGames.MachineUniformCopyOrder.occurrenceMajor line 106
  13. def OAI.DFVSGames.MachineUniformCopyOrder.copyMajor line 109
  14. theorem OAI.DFVSGames.MachineUniformCopyOrder.occurrenceMajor_perm_copyMajor line 112
  15. theorem OAI.DFVSGames.MachineUniformCopyOrder.selected_count_eq line 124
  16. theorem OAI.DFVSGames.MachineUniformCopyOrder.mem_iff line 130
  17. theorem OAI.DFVSGames.MachineUniformCopyOrder.copyMajor_selected_count line 134
  18. theorem OAI.DFVSGames.MachineUniformCopyOrder.occurrenceMajor_selected_count line 145
  19. theorem OAI.DFVSGames.MachineUniformCopyOrder.encoded_rows_perm line 150
  20. theorem OAI.DFVSGames.MachineUniformCopyOrder.countSatisfied_eq line 157
  21. def OAI.DFVSGames.Reduction.WeightRounding.floorMass line 169
  22. def OAI.DFVSGames.Reduction.WeightRounding.roundCounts line 172
  23. def OAI.DFVSGames.Reduction.WeightRounding.deficit line 177
  24. def OAI.DFVSGames.Reduction.WeightRounding.rounded line 179
  25. theorem OAI.DFVSGames.Reduction.WeightRounding.length_roundCounts line 182
  26. theorem OAI.DFVSGames.Reduction.WeightRounding.sum_roundCounts line 188
  27. theorem OAI.DFVSGames.Reduction.WeightRounding.floorMass_mul_le line 204
  28. theorem OAI.DFVSGames.Reduction.WeightRounding.scaled_sum_lt line 214
  29. theorem OAI.DFVSGames.Reduction.WeightRounding.floorMass_le_target line 230
  30. theorem OAI.DFVSGames.Reduction.WeightRounding.deficit_lt_length line 235
  31. theorem OAI.DFVSGames.Reduction.WeightRounding.sum_rounded line 245
  32. def OAI.DFVSGames.Reduction.WeightRounding.selectedSum line 253
  33. theorem OAI.DFVSGames.Reduction.WeightRounding.floor_entry_bounds line 258
  34. theorem OAI.DFVSGames.Reduction.WeightRounding.selected_roundCounts_error line 267
  35. theorem OAI.DFVSGames.Reduction.WeightRounding.selected_rounded_error line 292
  36. def OAI.DFVSGames.Reduction.WeightRounding.replicateOccurrences line 300
  37. theorem OAI.DFVSGames.Reduction.WeightRounding.length_replicateOccurrences line 304
  38. def OAI.DFVSGames.Reduction.WeightRounding.copyIndices line 312
  39. theorem OAI.DFVSGames.Reduction.WeightRounding.length_copyIndices line 316
  40. theorem OAI.DFVSGames.Reduction.WeightRounding.mem_copyIndices_lt line 321
  41. theorem OAI.DFVSGames.Reduction.WeightRounding.count_copyIndices line 336
  42. def OAI.DFVSGames.Reduction.WeightRounding.uniformSource line 345
  43. theorem OAI.DFVSGames.Reduction.WeightRounding.uniformSource_indices_lt line 347
  44. theorem OAI.DFVSGames.Reduction.WeightRounding.length_uniformSource line 352
  45. theorem OAI.DFVSGames.Reduction.WeightRounding.uniformSource_nonempty line 356
  46. theorem OAI.DFVSGames.Reduction.WeightRounding.uniformSource_error line 364
  47. def OAI.DFVSGames.Reduction.WeightRounding.ceilQuotient line 372
  48. theorem OAI.DFVSGames.Reduction.WeightRounding.le_ceilQuotient_mul line 374
  49. theorem OAI.DFVSGames.Reduction.WeightRounding.ceilQuotient_le line 382
  50. def OAI.DFVSGames.Reduction.WeightRounding.targetDenominator line 389
  51. theorem OAI.DFVSGames.Reduction.WeightRounding.targetDenominator_error_budget line 391
  52. theorem OAI.DFVSGames.Reduction.WeightRounding.targetDenominator_size line 395
  53. theorem OAI.DFVSGames.Reduction.WeightRounding.targetDenominator_positive line 400
  54. abbrev OAI.DFVSGames.Explicit.Rounding.IntegerRounding line 417
  55. def OAI.DFVSGames.Explicit.Rounding.denominator line 419
  56. theorem OAI.DFVSGames.Explicit.Rounding.denominator_budget line 421
  57. theorem OAI.DFVSGames.Explicit.Rounding.denominator_size line 425
  58. theorem OAI.DFVSGames.Explicit.Rounding.denominator_positive line 430
  59. def OAI.DFVSGames.Explicit.Rounding.remainder line 442
  60. def OAI.DFVSGames.Explicit.Rounding.priority line 445
  61. instance OAI.DFVSGames.Explicit.Rounding.priorityDecidable line 449
  62. instance OAI.DFVSGames.Explicit.Rounding.priorityTrans line 453
  63. instance OAI.DFVSGames.Explicit.Rounding.priorityAntisymm line 460
  64. instance OAI.DFVSGames.Explicit.Rounding.priorityTotal line 468
  65. def OAI.DFVSGames.Explicit.Rounding.remainderOrder line 475
  66. theorem OAI.DFVSGames.Explicit.Rounding.remainderOrder_sorted line 478
  67. theorem OAI.DFVSGames.Explicit.Rounding.remainderOrder_length line 482
  68. theorem OAI.DFVSGames.Explicit.Rounding.remainderOrder_nodup line 486
  69. def OAI.DFVSGames.Explicit.Rounding.floorCount line 489
  70. def OAI.DFVSGames.Explicit.Rounding.deficit line 492
  71. theorem OAI.DFVSGames.Explicit.Rounding.floor_sum_le line 495
  72. theorem OAI.DFVSGames.Explicit.Rounding.deficit_lt line 502
  73. def OAI.DFVSGames.Explicit.Rounding.incremented line 510
  74. def OAI.DFVSGames.Explicit.Rounding.count line 513
  75. theorem OAI.DFVSGames.Explicit.Rounding.incremented_card line 516
  76. theorem OAI.DFVSGames.Explicit.Rounding.sum_count line 522
  77. theorem OAI.DFVSGames.Explicit.Rounding.count_error line 531
  78. theorem OAI.DFVSGames.Explicit.Rounding.incremented_priority line 540
  79. theorem OAI.DFVSGames.Explicit.Rounding.selected_count_error line 557
  80. theorem OAI.DFVSGames.Explicit.Rounding.ratio_error line 567
  81. theorem OAI.DFVSGames.Explicit.Rounding.count_ratio_error line 581
  82. theorem OAI.DFVSGames.Explicit.Rounding.selected_ratio_error line 588
  83. theorem OAI.DFVSGames.Explicit.Rounding.denominator_ratio_budget line 599
  84. theorem OAI.DFVSGames.Explicit.Rounding.denominator_eq_ceil line 610
  85. theorem OAI.DFVSGames.Explicit.Rounding.selected_tolerance line 629
  86. theorem OAI.DFVSGames.Explicit.Rounding.selected_weight_error line 638
  87. theorem OAI.DFVSGames.Explicit.Rounding.selected_weight_tolerance line 645
  88. def OAI.DFVSGames.Explicit.Rounding.copies line 654
  89. theorem OAI.DFVSGames.Explicit.Rounding.copies_length line 657
  90. theorem OAI.DFVSGames.Explicit.Rounding.copies_nonempty line 661
  91. theorem OAI.DFVSGames.Explicit.Rounding.copies_filter_length line 669
  92. theorem OAI.DFVSGames.Explicit.Rounding.count_le line 675
  93. theorem OAI.DFVSGames.MachineUniformRounding.denominator_uniform line 690
  94. theorem OAI.DFVSGames.MachineUniformRounding.denominator_uniform_eq_ceil line 694
  95. theorem OAI.DFVSGames.MachineUniformRounding.uniform_mass line 699
  96. theorem OAI.DFVSGames.MachineUniformRounding.scaled_quota_uniform line 701
  97. theorem OAI.DFVSGames.MachineUniformRounding.floorCount_uniform line 708
  98. theorem OAI.DFVSGames.MachineUniformRounding.remainder_uniform line 712
  99. theorem OAI.DFVSGames.MachineUniformRounding.deficit_uniform line 716
  100. theorem OAI.DFVSGames.MachineUniformRounding.incremented_uniform line 721
  101. theorem OAI.DFVSGames.MachineUniformRounding.count_uniform line 725
  102. theorem OAI.DFVSGames.MachineUniformRounding.copies_uniform line 730
  103. theorem OAI.DFVSGames.MachineUniformRounding.copies_uniform_length line 735
  104. theorem OAI.DFVSGames.MachineUniformRounding.normalized_count_uniform line 739
  105. theorem OAI.DFVSGames.MachineUniformRounding.selected_weights_exact line 749
  106. def OAI.DFVSGames.Integration.DyadicErrors.dyadicError line 764
  107. theorem OAI.DFVSGames.Integration.DyadicErrors.errorValue_dyadic line 774
  108. theorem OAI.DFVSGames.Integration.DyadicErrors.exists_dyadic_below_real line 778
  109. theorem OAI.DFVSGames.Integration.DyadicErrors.exists_dyadic_below line 790
  110. theorem OAI.DFVSGames.Integration.DyadicErrors.completeAt_real_of_dyadic line 796
  111. theorem OAI.DFVSGames.Integration.DyadicErrors.soundAt_real_of_dyadic line 804