OAI/Computability/DirectedFeedback/RankGraph/AllGraph.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectedFeedback.Construction.AllVertex line 16
  2. instance OAI.DirectedFeedback.Construction.rawFullFintype line 17
  3. instance OAI.DirectedFeedback.Construction.rawBigFintype line 18
  4. instance OAI.DirectedFeedback.Construction.rawSmallFintype line 19
  5. instance OAI.DirectedFeedback.Construction.rawCompareFintype line 20
  6. instance OAI.DirectedFeedback.Construction.allVertexFintype line 21
  7. def OAI.DirectedFeedback.Construction.supportEmbed line 27
  8. def OAI.DirectedFeedback.Construction.allCost line 32
  9. def OAI.DirectedFeedback.Construction.AllArc line 39
  10. theorem OAI.DirectedFeedback.Construction.supportEmbed_injective line 42
  11. theorem OAI.DirectedFeedback.Construction.embed_arc line 51
  12. theorem OAI.DirectedFeedback.Construction.allCost_sum line 61
  13. theorem OAI.DirectedFeedback.Construction.all_soundness line 73
  14. structure OAI.DirectedFeedback.GraphPrinter.Family line 105
  15. def OAI.DirectedFeedback.GraphPrinter.Family.pairs line 118
  16. theorem OAI.DirectedFeedback.GraphPrinter.Family.mem_pairs line 122
  17. def OAI.DirectedFeedback.GraphPrinter.Family.graph line 125
  18. def OAI.DirectedFeedback.GraphPrinter.Family.inst line 136
  19. def OAI.DirectedFeedback.GraphPrinter.Family.count line 138
  20. theorem OAI.DirectedFeedback.GraphPrinter.Family.count_eq line 141
  21. theorem OAI.DirectedFeedback.GraphPrinter.Family.flatMap_filter line 150
  22. theorem OAI.DirectedFeedback.GraphPrinter.Family.map_fin_values line 157
  23. def OAI.DirectedFeedback.GraphPrinter.Family.edgeBits line 163
  24. theorem OAI.DirectedFeedback.GraphPrinter.Family.edgeBits_eq line 167
  25. theorem OAI.DirectedFeedback.GraphPrinter.Family.n_def_any line 179
  26. theorem OAI.DirectedFeedback.GraphPrinter.Family.count_def line 182
  27. theorem OAI.DirectedFeedback.GraphPrinter.Family.edgeBits_def line 188
  28. def OAI.DirectedFeedback.GraphPrinter.Family.bits line 197
  29. theorem OAI.DirectedFeedback.GraphPrinter.Family.bits_def line 200
  30. theorem OAI.DirectedFeedback.GraphPrinter.Family.bits_correct line 207
  31. def OAI.DirectedFeedback.GraphPrinter.Family.computation line 213
  32. theorem OAI.DirectedFeedback.GraphPrinter.Family.computation_finite line 220
  33. def OAI.DirectedFeedback.LocalAssignments.Consistent line 236
  34. theorem OAI.DirectedFeedback.LocalAssignments.extend_global line 239
  35. theorem OAI.DirectedFeedback.LocalAssignments.restriction_consistent line 249
  36. theorem OAI.DirectedFeedback.LocalAssignments.forall_iff line 252
  37. theorem OAI.DirectedFeedback.LocalAssignments.Definability.consistent_def line 269
  38. abbrev OAI.DirectedFeedback.LocalPrinter.Rule line 288
  39. def OAI.DirectedFeedback.LocalPrinter.Ordered line 290
  40. def OAI.DirectedFeedback.LocalPrinter.potential line 294
  41. theorem OAI.DirectedFeedback.LocalPrinter.ordered_iff line 296
  42. structure OAI.DirectedFeedback.LocalPrinter.Family line 300
  43. def OAI.DirectedFeedback.LocalPrinter.Family.Arc line 320
  44. def OAI.DirectedFeedback.LocalPrinter.Family.value line 328
  45. theorem OAI.DirectedFeedback.LocalPrinter.Family.arc_global line 331
  46. theorem OAI.DirectedFeedback.LocalPrinter.Family.arc_def line 346
  47. def OAI.DirectedFeedback.LocalPrinter.Family.printer line 367
  48. def OAI.DirectedFeedback.LocalPrinter.Family.deleted line 377
  49. theorem OAI.DirectedFeedback.LocalPrinter.Family.deleted_feedback line 380
  50. abbrev OAI.DirectedFeedback.AllLabels.deleted line 414
  51. abbrev OAI.DirectedFeedback.AllLabels.pot line 416
  52. def OAI.DirectedFeedback.AllLabels.height line 419
  53. theorem OAI.DirectedFeedback.AllLabels.height_bound line 425
  54. def OAI.DirectedFeedback.AllLabels.code line 439
  55. theorem OAI.DirectedFeedback.AllLabels.code_none line 443
  56. theorem OAI.DirectedFeedback.AllLabels.height_potential line 447
  57. theorem OAI.DirectedFeedback.AllLabels.ordered_arc line 452
  58. theorem OAI.DirectedFeedback.AllLabels.embed_deleted line 466
  59. theorem OAI.DirectedFeedback.AllLabels.completeness line 474
  60. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.fixed_denominator line 502
  61. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.integral_realization line 520
  62. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pushforward_comp line 530
  63. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pushforward_product line 543
  64. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pushforward_fst line 556
  65. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.eq_of_expectation_eq line 576
  66. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.zipEquiv line 582
  67. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.iid_zip line 589
  68. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_zip line 598
  69. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_map line 606
  70. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.sample_prefix line 612
  71. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.sample_prefix_fresh line 627
  72. abbrev OAI.DirectedFeedback.PacketSeeds.SlotSeed line 657
  73. abbrev OAI.DirectedFeedback.PacketSeeds.PrefixSeed line 658
  74. abbrev OAI.DirectedFeedback.PacketSeeds.FullSeed line 659
  75. abbrev OAI.DirectedFeedback.PacketSeeds.CommonSeed line 661
  76. abbrev OAI.DirectedFeedback.PacketSeeds.BigSeed line 663
  77. abbrev OAI.DirectedFeedback.PacketSeeds.SmallSeed line 665
  78. abbrev OAI.DirectedFeedback.PacketSeeds.CompareSeed line 667
  79. abbrev OAI.DirectedFeedback.PacketSeeds.Seed line 670
  80. instance OAI.DirectedFeedback.PacketSeeds.seedFullFintype line 672
  81. instance OAI.DirectedFeedback.PacketSeeds.seedCommonFintype line 673
  82. instance OAI.DirectedFeedback.PacketSeeds.seedBigFintype line 674
  83. instance OAI.DirectedFeedback.PacketSeeds.seedSmallFintype line 675
  84. instance OAI.DirectedFeedback.PacketSeeds.seedCompareFintype line 676
  85. instance OAI.DirectedFeedback.PacketSeeds.seedFintype line 677
  86. def OAI.DirectedFeedback.PacketSeeds.slotLaw line 679
  87. def OAI.DirectedFeedback.PacketSeeds.fullLaw line 682
  88. def OAI.DirectedFeedback.PacketSeeds.commonLaw line 683
  89. def OAI.DirectedFeedback.PacketSeeds.bigLaw line 685
  90. def OAI.DirectedFeedback.PacketSeeds.smallLaw line 686
  91. def OAI.DirectedFeedback.PacketSeeds.localCompareLaw line 688
  92. def OAI.DirectedFeedback.PacketSeeds.compareLaw line 691
  93. def OAI.DirectedFeedback.PacketSeeds.fillPrefix line 696
  94. def OAI.DirectedFeedback.PacketSeeds.fillFull line 698
  95. def OAI.DirectedFeedback.PacketSeeds.fillCommon line 700
  96. def OAI.DirectedFeedback.PacketSeeds.fresh line 702
  97. def OAI.DirectedFeedback.PacketSeeds.fillBig line 704
  98. def OAI.DirectedFeedback.PacketSeeds.fillSmall line 706
  99. def OAI.DirectedFeedback.PacketSeeds.fillCompare line 708
  100. def OAI.DirectedFeedback.PacketSeeds.fill line 711
  101. theorem OAI.DirectedFeedback.PacketSeeds.sample_full line 718
  102. theorem OAI.DirectedFeedback.PacketSeeds.sample_big line 727
  103. theorem OAI.DirectedFeedback.PacketSeeds.sample_small line 742
  104. theorem OAI.DirectedFeedback.PacketSeeds.sample_compare line 757
  105. abbrev OAI.DirectedFeedback.RankPackets.Shape line 788
  106. instance OAI.DirectedFeedback.RankPackets.shapeFintype line 792
  107. def OAI.DirectedFeedback.RankPackets.fill line 797
  108. theorem OAI.DirectedFeedback.RankPackets.fill_surjective line 803
  109. theorem OAI.DirectedFeedback.RankPackets.eval_fill line 826