OAI/Computability/DirectedFeedback/RankGraph/Bias.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Games.listChoice_weight line 44
  2. theorem OAI.DirectedFeedback.Games.listChoice_pair_success line 49
  3. theorem OAI.DirectedFeedback.Games.randomized_score line 71
  4. theorem OAI.DirectedFeedback.Games.list_decoding line 90
  5. def OAI.DirectedFeedback.Construction.bias line 135
  6. theorem OAI.DirectedFeedback.Construction.bias_pos line 138
  7. theorem OAI.DirectedFeedback.Construction.bias_le_quarter line 141
  8. def OAI.DirectedFeedback.Construction.subsetLaw line 148
  9. abbrev OAI.DirectedFeedback.Construction.Slot line 151
  10. abbrev OAI.DirectedFeedback.Construction.PrefixData line 152
  11. def OAI.DirectedFeedback.Construction.sets line 154
  12. def OAI.DirectedFeedback.Construction.cell line 157
  13. def OAI.DirectedFeedback.Construction.vertices line 160
  14. abbrev OAI.DirectedFeedback.Construction.Emb line 162
  15. def OAI.DirectedFeedback.Construction.maxCells line 163
  16. def OAI.DirectedFeedback.Construction.rankLength line 164
  17. abbrev OAI.DirectedFeedback.Construction.Common line 166
  18. abbrev OAI.DirectedFeedback.Construction.Full line 168
  19. abbrev OAI.DirectedFeedback.Construction.Big line 170
  20. abbrev OAI.DirectedFeedback.Construction.Small line 172
  21. abbrev OAI.DirectedFeedback.Construction.Compare line 174
  22. abbrev OAI.DirectedFeedback.Construction.Wild line 177
  23. def OAI.DirectedFeedback.Construction.bigMarginal line 180
  24. def OAI.DirectedFeedback.Construction.smallMarginal line 181
  25. def OAI.DirectedFeedback.Construction.common line 183
  26. def OAI.DirectedFeedback.Construction.fullLaw line 186
  27. def OAI.DirectedFeedback.Construction.bigLaw line 189
  28. def OAI.DirectedFeedback.Construction.smallLaw line 193
  29. instance OAI.DirectedFeedback.Construction.cellCountNeZero line 197
  30. def OAI.DirectedFeedback.Construction.comparisonLaw line 200
  31. theorem OAI.DirectedFeedback.Construction.cellCount_mono line 207
  32. theorem OAI.DirectedFeedback.Construction.full_cells_bound line 212
  33. theorem OAI.DirectedFeedback.Construction.ordered_cells_bound line 217
  34. def OAI.DirectedFeedback.Construction.level line 225
  35. def OAI.DirectedFeedback.Construction.fullCount line 228
  36. def OAI.DirectedFeedback.Construction.fullStars line 231
  37. def OAI.DirectedFeedback.Construction.fullWildcard line 234
  38. def OAI.DirectedFeedback.Construction.bigWildcard line 242
  39. def OAI.DirectedFeedback.Construction.smallWildcard line 251
  40. def OAI.DirectedFeedback.Construction.wildcard line 259
  41. def OAI.DirectedFeedback.Construction.comparison line 265
  42. abbrev OAI.DirectedFeedback.SourceProbability.FiniteDistribution.Support line 288
  43. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.sum_support line 290
  44. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.supported line 301
  45. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_supported line 306
  46. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_supported line 309
  47. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.extend line 314
  48. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.extend_at_support line 317
  49. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_extend line 320
  50. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.support_nonempty line 325
  51. instance OAI.DirectedFeedback.Construction.rankFintype line 344
  52. abbrev OAI.DirectedFeedback.Construction.WildSupport line 348
  53. abbrev OAI.DirectedFeedback.Construction.ComparisonSupport line 350
  54. abbrev OAI.DirectedFeedback.Construction.OutputVertex line 351
  55. def OAI.DirectedFeedback.Construction.forgetWild line 354
  56. def OAI.DirectedFeedback.Construction.wildSupport line 359
  57. def OAI.DirectedFeedback.Construction.compSupport line 362
  58. def OAI.DirectedFeedback.Construction.OutputArc line 365
  59. theorem OAI.DirectedFeedback.Construction.output_loopless line 368
  60. def OAI.DirectedFeedback.Construction.vertexCost line 372
  61. theorem OAI.DirectedFeedback.Construction.vertexCost_pos line 379
  62. instance OAI.DirectedFeedback.Construction.fullSupportFintype line 389
  63. instance OAI.DirectedFeedback.Construction.bigSupportFintype line 390
  64. instance OAI.DirectedFeedback.Construction.smallSupportFintype line 391
  65. instance OAI.DirectedFeedback.Construction.comparisonSupportFintype line 392
  66. instance OAI.DirectedFeedback.Construction.outputFintype line 394
  67. def OAI.DirectedFeedback.Construction.totalDeletionCost line 398
  68. def OAI.DirectedFeedback.Construction.fullDeleted line 401
  69. def OAI.DirectedFeedback.Construction.bigDeleted line 403
  70. def OAI.DirectedFeedback.Construction.smallDeleted line 405
  71. def OAI.DirectedFeedback.Construction.comparisonDeleted line 407
  72. theorem OAI.DirectedFeedback.Construction.deletionCost_decomposition line 410
  73. theorem OAI.DirectedFeedback.Construction.rank_retained line 427
  74. def OAI.DirectedFeedback.Prefix.normalizedCondition line 449
  75. theorem OAI.DirectedFeedback.Prefix.normalized_eq line 455
  76. theorem OAI.DirectedFeedback.Prefix.normalized_properties line 462
  77. def OAI.DirectedFeedback.RankGraph.conditionedSmall line 491
  78. theorem OAI.DirectedFeedback.RankGraph.conditionedSmall_properties line 498
  79. def OAI.DirectedFeedback.RankGraph.bigStepBit line 509
  80. theorem OAI.DirectedFeedback.RankGraph.bigStepBit_lift line 514
  81. def OAI.DirectedFeedback.RankGraph.conditionedBig line 527
  82. theorem OAI.DirectedFeedback.RankGraph.conditionedBig_properties line 534
  83. theorem OAI.DirectedFeedback.Prefix.starred_transition_crosses line 552
  84. theorem OAI.DirectedFeedback.Prefix.unstarred_transition_exists line 576
  85. abbrev OAI.DirectedFeedback.Construction.rankOrder line 606
  86. theorem OAI.DirectedFeedback.Construction.rankOrder_arc line 609
  87. theorem OAI.DirectedFeedback.Construction.rankLength_ge line 614
  88. theorem OAI.DirectedFeedback.Construction.full_unstarred line 616
  89. def OAI.DirectedFeedback.Construction.bigFunction line 641
  90. def OAI.DirectedFeedback.Construction.smallFunction line 646
  91. def OAI.DirectedFeedback.Construction.commonTransition line 651
  92. theorem OAI.DirectedFeedback.Construction.comparison_forces_deletion line 657
  93. theorem OAI.DirectedFeedback.Pivotal.omitted_crossing line 689
  94. theorem OAI.DirectedFeedback.RankGraph.ordered_wildcard_forcing line 721
  95. def OAI.DirectedFeedback.Construction.bigGood line 768
  96. def OAI.DirectedFeedback.Construction.smallGood line 771
  97. theorem OAI.DirectedFeedback.Construction.small_forces_deletion line 775
  98. theorem OAI.DirectedFeedback.Construction.big_forces_deletion line 799
  99. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_mono_support line 831
  100. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_mono_support line 841
  101. theorem OAI.DirectedFeedback.Pivotal.labelOrder_weight_pos line 856
  102. theorem OAI.DirectedFeedback.Pivotal.averaged_budget_charge_support line 860
  103. theorem OAI.DirectedFeedback.Pivotal.subset_function_properties line 886