OAI/Computability/DirectedFeedback/RankGraph/Rational.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Construction.parameterized_soundness line 62
  2. theorem OAI.DirectedFeedback.Construction.parameterized_completeness line 84
  3. def OAI.DirectedFeedback.Rational line 105
  4. theorem OAI.DirectedFeedback.Rational.rat line 108
  5. theorem OAI.DirectedFeedback.Rational.nat line 109
  6. theorem OAI.DirectedFeedback.Rational.zero line 110
  7. theorem OAI.DirectedFeedback.Rational.one line 111
  8. theorem OAI.DirectedFeedback.Rational.add line 112
  9. theorem OAI.DirectedFeedback.Rational.sub line 115
  10. theorem OAI.DirectedFeedback.Rational.mul line 118
  11. theorem OAI.DirectedFeedback.Rational.inv line 121
  12. theorem OAI.DirectedFeedback.Rational.div line 124
  13. theorem OAI.DirectedFeedback.Rational.pow line 126
  14. theorem OAI.DirectedFeedback.Rational.sum line 129
  15. theorem OAI.DirectedFeedback.Rational.prod line 136
  16. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass line 149
  17. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.uniform line 151
  18. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.product line 154
  19. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.sigma line 158
  20. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.iid line 163
  21. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.table line 169
  22. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.RationalMass.pushforward line 173
  23. theorem OAI.DirectedFeedback.Construction.subsetLaw_rational line 191
  24. theorem OAI.DirectedFeedback.Construction.common_rational line 205
  25. theorem OAI.DirectedFeedback.Construction.fullLaw_rational line 213
  26. theorem OAI.DirectedFeedback.Construction.bigLaw_rational line 219
  27. theorem OAI.DirectedFeedback.Construction.smallLaw_rational line 224
  28. theorem OAI.DirectedFeedback.Construction.comparisonLaw_rational line 229
  29. theorem OAI.DirectedFeedback.Construction.vertexCost_rational line 245
  30. theorem OAI.DirectedFeedback.Digraph.dfvs_le_iff line 262
  31. theorem OAI.DirectedFeedback.Digraph.dfvs_attained line 273
  32. def OAI.DirectedFeedback.graphOfRelation line 281
  33. theorem OAI.DirectedFeedback.graphOfRelation_mem line 293
  34. theorem OAI.DirectedFeedback.graphOfRelation_feedback line 302
  35. theorem OAI.DirectedFeedback.relation_feedback_of_graph line 312
  36. theorem OAI.DirectedFeedback.graphOfRelation_dfvs_le_iff line 326
  37. theorem OAI.DirectedFeedback.cloneRel_irrefl line 339
  38. def OAI.DirectedFeedback.roundedGraph line 342
  39. theorem OAI.DirectedFeedback.roundedGraph_yes line 346
  40. theorem OAI.DirectedFeedback.roundedGraph_no line 357
  41. def OAI.DirectedFeedback.Construction.rationalCost line 378
  42. theorem OAI.DirectedFeedback.Construction.rationalCost_cast line 381
  43. theorem OAI.DirectedFeedback.Construction.rationalCost_pos line 386
  44. theorem OAI.DirectedFeedback.Construction.cost_sum line 393
  45. instance OAI.DirectedFeedback.Construction.parameterized_output_nonempty line 398
  46. def OAI.DirectedFeedback.Construction.unweightedInstance line 404
  47. theorem OAI.DirectedFeedback.Construction.unweighted_yes line 410
  48. theorem OAI.DirectedFeedback.Construction.unweighted_no line 421
  49. def OAI.DirectedFeedback.UGBridge.game line 456
  50. def OAI.DirectedFeedback.UGBridge.fiber line 462
  51. theorem OAI.DirectedFeedback.UGBridge.fiber_project line 466
  52. theorem OAI.DirectedFeedback.UGBridge.alphabet_card line 470
  53. theorem OAI.DirectedFeedback.UGBridge.rational line 473
  54. theorem OAI.DirectedFeedback.UGBridge.score_eq line 477
  55. abbrev OAI.DirectedFeedback.SourceInstance.UG line 490
  56. abbrev OAI.DirectedFeedback.SourceInstance.Left line 491
  57. abbrev OAI.DirectedFeedback.SourceInstance.Right line 492
  58. abbrev OAI.DirectedFeedback.SourceInstance.Edge line 493
  59. instance OAI.DirectedFeedback.SourceInstance.edge_nonempty line 495
  60. instance OAI.DirectedFeedback.SourceInstance.label_nonempty line 497
  61. def OAI.DirectedFeedback.SourceInstance.game line 500
  62. def OAI.DirectedFeedback.SourceInstance.fiber line 501
  63. theorem OAI.DirectedFeedback.SourceInstance.correct line 503
  64. theorem OAI.DirectedFeedback.SourceInstance.sound line 515
  65. def OAI.DirectedFeedback.FromUG.instanceOf line 536
  66. theorem OAI.DirectedFeedback.FromUG.yes line 540
  67. theorem OAI.DirectedFeedback.FromUG.no line 545
  68. theorem OAI.DirectedFeedback.FromUG.exists_correct_map line 550
  69. abbrev OAI.DirectedFeedback.FullGame.Edge line 575
  70. instance OAI.DirectedFeedback.FullGame.edge_nonempty line 576
  71. instance OAI.DirectedFeedback.FullGame.vertex_nonempty line 577
  72. def OAI.DirectedFeedback.FullGame.game line 580
  73. def OAI.DirectedFeedback.FullGame.fiber line 586
  74. theorem OAI.DirectedFeedback.FullGame.fiber_project line 589
  75. theorem OAI.DirectedFeedback.FullGame.score_restrict line 594
  76. theorem OAI.DirectedFeedback.FullGame.completeness line 599
  77. theorem OAI.DirectedFeedback.FullGame.soundness line 611
  78. def OAI.DirectedFeedback.GameRead.n line 629
  79. def OAI.DirectedFeedback.GameRead.m line 630
  80. def OAI.DirectedFeedback.GameRead.field line 631
  81. def OAI.DirectedFeedback.GameRead.left line 632
  82. def OAI.DirectedFeedback.GameRead.right line 633
  83. def OAI.DirectedFeedback.GameRead.table line 634
  84. def OAI.DirectedFeedback.GameRead.asPerm line 636
  85. def OAI.DirectedFeedback.GameRead.perm line 638
  86. def OAI.DirectedFeedback.GameRead.fiber line 639
  87. theorem OAI.DirectedFeedback.GameRead.n_pos line 642
  88. theorem OAI.DirectedFeedback.GameRead.m_pos line 643
  89. theorem OAI.DirectedFeedback.GameRead.n_def line 645
  90. theorem OAI.DirectedFeedback.GameRead.m_def line 646
  91. theorem OAI.DirectedFeedback.GameRead.field_def line 648
  92. theorem OAI.DirectedFeedback.GameRead.left_def line 652
  93. theorem OAI.DirectedFeedback.GameRead.right_def line 655
  94. theorem OAI.DirectedFeedback.GameRead.table_def line 657
  95. theorem OAI.DirectedFeedback.GameRead.perm_def line 665
  96. theorem OAI.DirectedFeedback.GameRead.fiber_def line 667
  97. lemma OAI.DirectedFeedback.GameRead.word_game line 671
  98. theorem OAI.DirectedFeedback.GameRead.n_encoded line 675
  99. theorem OAI.DirectedFeedback.GameRead.m_encoded line 683
  100. lemma OAI.DirectedFeedback.GameRead.get_flatMap line 690
  101. theorem OAI.DirectedFeedback.GameRead.field_encoded line 708
  102. theorem OAI.DirectedFeedback.GameRead.left_encoded line 721
  103. theorem OAI.DirectedFeedback.GameRead.right_encoded line 729
  104. theorem OAI.DirectedFeedback.GameRead.table_encoded line 736
  105. theorem OAI.DirectedFeedback.GameRead.perm_encoded line 751
  106. theorem OAI.DirectedFeedback.GameRead.fiber_encoded line 758
  107. def OAI.DirectedFeedback.PotentialCover.fullFibers line 773
  108. theorem OAI.DirectedFeedback.PotentialCover.mem_fullFibers line 776
  109. theorem OAI.DirectedFeedback.PotentialCover.feedback_project line 779
  110. def OAI.DirectedFeedback.PotentialCover.fiberCount line 798
  111. theorem OAI.DirectedFeedback.PotentialCover.fullFibers_cost_le line 800
  112. theorem OAI.DirectedFeedback.PotentialCover.weight_le_card line 814
  113. def OAI.DirectedFeedback.PotentialCover.Arc line 824
  114. theorem OAI.DirectedFeedback.PotentialCover.irrefl line 828
  115. theorem OAI.DirectedFeedback.PotentialCover.deleted_feedback line 831
  116. theorem OAI.DirectedFeedback.PotentialCover.covers line 844