OAI/Computability/DirectedFeedback/RankGraph/PacketLocality.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectedFeedback.PacketLocality.Slots line 16
  2. def OAI.DirectedFeedback.PacketLocality.localGame line 17
  3. lemma OAI.DirectedFeedback.PacketLocality.comp_snoc line 26
  4. lemma OAI.DirectedFeedback.PacketLocality.map_snoc_apply line 29
  5. lemma OAI.DirectedFeedback.PacketLocality.deleted_fill line 34
  6. lemma OAI.DirectedFeedback.PacketLocality.height_fill line 50
  7. lemma OAI.DirectedFeedback.PacketLocality.code_fill line 66
  8. abbrev OAI.DirectedFeedback.RawFamily.X line 89
  9. abbrev OAI.DirectedFeedback.RawFamily.Y line 90
  10. abbrev OAI.DirectedFeedback.RawFamily.Shape line 91
  11. abbrev OAI.DirectedFeedback.RawFamily.Seed line 92
  12. abbrev OAI.DirectedFeedback.RawFamily.Tag line 93
  13. instance OAI.DirectedFeedback.RawFamily.tagNonempty line 94
  14. theorem OAI.DirectedFeedback.RawFamily.hYX line 96
  15. def OAI.DirectedFeedback.RawFamily.scale line 98
  16. def OAI.DirectedFeedback.RawFamily.r line 99
  17. def OAI.DirectedFeedback.RawFamily.base line 100
  18. def OAI.DirectedFeedback.RawFamily.copies line 101
  19. def OAI.DirectedFeedback.RawFamily.size line 103
  20. def OAI.DirectedFeedback.RawFamily.tag line 105
  21. def OAI.DirectedFeedback.RawFamily.digit line 107
  22. def OAI.DirectedFeedback.RawFamily.copy line 109
  23. def OAI.DirectedFeedback.RawFamily.valid line 111
  24. def OAI.DirectedFeedback.RawFamily.isRank line 114
  25. def OAI.DirectedFeedback.RawFamily.u line 115
  26. def OAI.DirectedFeedback.RawFamily.v line 118
  27. def OAI.DirectedFeedback.RawFamily.tagRule line 122
  28. def OAI.DirectedFeedback.RawFamily.rule line 128
  29. theorem OAI.DirectedFeedback.RawFamily.scale_def line 132
  30. theorem OAI.DirectedFeedback.RawFamily.r_def line 135
  31. theorem OAI.DirectedFeedback.RawFamily.base_def line 137
  32. theorem OAI.DirectedFeedback.RawFamily.copies_def line 140
  33. theorem OAI.DirectedFeedback.RawFamily.size_def line 143
  34. theorem OAI.DirectedFeedback.RawFamily.tag_def line 147
  35. theorem OAI.DirectedFeedback.RawFamily.digit_def line 150
  36. theorem OAI.DirectedFeedback.RawFamily.copy_def line 153
  37. theorem OAI.DirectedFeedback.RawFamily.isRank_def line 156
  38. theorem OAI.DirectedFeedback.RawFamily.u_def line 159
  39. theorem OAI.DirectedFeedback.RawFamily.v_def line 163
  40. theorem OAI.DirectedFeedback.RawFamily.rule_def line 167
  41. theorem OAI.DirectedFeedback.RawFamily.valid_def line 171
  42. def OAI.DirectedFeedback.RawFamily.family line 187
  43. def OAI.DirectedFeedback.PacketSeeds.mass line 218
  44. theorem OAI.DirectedFeedback.PacketSeeds.mass_nonnegative line 224
  45. theorem OAI.DirectedFeedback.PacketSeeds.slot_rational line 228
  46. theorem OAI.DirectedFeedback.PacketSeeds.common_rational line 232
  47. theorem OAI.DirectedFeedback.PacketSeeds.localCompare_rational line 236
  48. theorem OAI.DirectedFeedback.PacketSeeds.mass_rational line 249
  49. theorem OAI.DirectedFeedback.PacketSeeds.denominator line 260
  50. theorem OAI.DirectedFeedback.PacketSeeds.moment line 266
  51. theorem OAI.DirectedFeedback.PacketSeeds.iid_uniform_expectation line 291
  52. theorem OAI.DirectedFeedback.PacketSeeds.integer_moment line 299
  53. abbrev OAI.DirectedFeedback.LivePackets.Live line 328
  54. instance OAI.DirectedFeedback.LivePackets.liveFintype line 331
  55. def OAI.DirectedFeedback.LivePackets.project line 337
  56. theorem OAI.DirectedFeedback.LivePackets.sum_project line 342
  57. theorem OAI.DirectedFeedback.LivePackets.sum_cost line 350
  58. theorem OAI.DirectedFeedback.LivePackets.rank_fiber_bound line 359
  59. theorem OAI.DirectedFeedback.LivePackets.test_fiber_count line 379
  60. theorem OAI.DirectedFeedback.LivePackets.fiber_weight line 390
  61. def OAI.DirectedFeedback.FiniteLift.pull line 417
  62. theorem OAI.DirectedFeedback.FiniteLift.pull_card line 419
  63. theorem OAI.DirectedFeedback.FiniteLift.pull_feedback line 424
  64. theorem OAI.DirectedFeedback.FiniteLift.feedback_cost line 430
  65. abbrev OAI.DirectedFeedback.RawFamily.W line 456
  66. abbrev OAI.DirectedFeedback.RawFamily.E line 457
  67. instance OAI.DirectedFeedback.RawFamily.wNonempty line 458
  68. instance OAI.DirectedFeedback.RawFamily.eNonempty line 459
  69. abbrev OAI.DirectedFeedback.RawFamily.Live line 460
  70. def OAI.DirectedFeedback.RawFamily.embed line 462
  71. theorem OAI.DirectedFeedback.RawFamily.embed_injective line 466
  72. theorem OAI.DirectedFeedback.RawFamily.valid_embed line 468
  73. theorem OAI.DirectedFeedback.RawFamily.valid_surjective line 471
  74. theorem OAI.DirectedFeedback.RawFamily.tag_embed line 476
  75. theorem OAI.DirectedFeedback.RawFamily.digit_embed line 483
  76. theorem OAI.DirectedFeedback.RawFamily.value_embed line 497
  77. theorem OAI.DirectedFeedback.RawFamily.cover_arc line 521
  78. def OAI.DirectedFeedback.RawFamily.liveDeleted line 535
  79. theorem OAI.DirectedFeedback.RawFamily.deleted_eq_image line 539
  80. def OAI.DirectedFeedback.RawFamily.extend line 580
  81. theorem OAI.DirectedFeedback.RawFamily.extend_restrict line 582
  82. theorem OAI.DirectedFeedback.RawFamily.feedback_printer_iff line 585
  83. theorem OAI.DirectedFeedback.RawFamily.live_card_bound line 598
  84. theorem OAI.DirectedFeedback.RawFamily.completeness line 615
  85. theorem OAI.DirectedFeedback.RawFamily.soundness line 633
  86. def OAI.DirectedFeedback.RawFamily.Model line 673
  87. lemma OAI.DirectedFeedback.RawFamily.encoded_model line 680
  88. theorem OAI.DirectedFeedback.RawFamily.encoded_yes line 702
  89. theorem OAI.DirectedFeedback.RawFamily.encoded_no line 710