OAI/Computability/DirectedFeedback/RankGraph/Point.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Pivotal.acceptance_le_mul_budget line 27
  2. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_or_le_add line 50
  3. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_exists_le_sum line 58
  4. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_not line 76
  5. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.indicator_difference line 85
  6. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_disagree_triangle line 94
  7. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_abs_sub_le_disagree line 108
  8. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pair_event_disagree line 120
  9. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.point line 142
  10. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_point line 147
  11. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_sub line 150
  12. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_mul_right line 154
  13. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_eq_expect line 158
  14. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.sigma line 162
  15. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_sigma line 170
  16. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.bind line 175
  17. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_bind line 178
  18. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_transport line 182
  19. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.uniform_transport line 189
  20. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.uniform_pushforward line 195
  21. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.uniform_product line 205
  22. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_ge_atom line 211
  23. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_uniform line 220
  24. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_table_pair line 225
  25. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_product_pattern line 233
  26. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.markov_bound line 244
  27. def OAI.DirectedFeedback.Pivotal.insertOrder line 263
  28. theorem OAI.DirectedFeedback.Pivotal.insertOrder_self line 267
  29. theorem OAI.DirectedFeedback.Pivotal.insertOrder_other line 272
  30. def OAI.DirectedFeedback.Pivotal.deleteOrder line 276
  31. theorem OAI.DirectedFeedback.Pivotal.deleteOrder_spec line 280
  32. theorem OAI.DirectedFeedback.Pivotal.insert_delete_order line 287
  33. theorem OAI.DirectedFeedback.Pivotal.delete_insert_order line 296
  34. def OAI.DirectedFeedback.Pivotal.orderDecomposition line 304
  35. def OAI.DirectedFeedback.Pivotal.orderHit line 310
  36. def OAI.DirectedFeedback.Pivotal.omittedHit line 314
  37. theorem OAI.DirectedFeedback.Pivotal.succAbove_cut_forward line 319
  38. theorem OAI.DirectedFeedback.Pivotal.succAbove_cut_backward line 324
  39. theorem OAI.DirectedFeedback.Pivotal.omittedHit_insert line 329
  40. def OAI.DirectedFeedback.Pivotal.permutationOrder line 349
  41. theorem OAI.DirectedFeedback.Pivotal.orderHit_permutation line 355
  42. instance OAI.DirectedFeedback.Pivotal.nonemptyOrder line 358
  43. theorem OAI.DirectedFeedback.Pivotal.uniform_deleting line 361
  44. abbrev OAI.DirectedFeedback.Pivotal.LabelOrder line 387
  45. instance OAI.DirectedFeedback.Pivotal.labelOrderNonempty line 390
  46. def OAI.DirectedFeedback.Pivotal.labelOrderLaw line 393
  47. theorem OAI.DirectedFeedback.Pivotal.labelOrder_hit_probability line 396
  48. theorem OAI.DirectedFeedback.Pivotal.single_label_budget_charge line 404
  49. theorem OAI.DirectedFeedback.Pivotal.budget_nonneg line 413
  50. theorem OAI.DirectedFeedback.Pivotal.budget_le_card line 417
  51. theorem OAI.DirectedFeedback.Pivotal.averaged_budget_charge line 422
  52. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.splitSnoc line 453
  53. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.iid_snoc_transport line 459
  54. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_snoc line 468
  55. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.takePrefix line 476
  56. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.takePrefix_self line 480
  57. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.take_snoc_eq line 483
  58. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_take line 489
  59. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_prefix_fresh line 506
  60. abbrev OAI.DirectedFeedback.PrefixExperiment.Atom line 524
  61. def OAI.DirectedFeedback.PrefixExperiment.atomLaw line 526
  62. theorem OAI.DirectedFeedback.PrefixExperiment.fresh_index_expectation line 529
  63. def OAI.DirectedFeedback.PrefixExperiment.commonLaw line 548
  64. def OAI.DirectedFeedback.PrefixExperiment.count line 553
  65. def OAI.DirectedFeedback.PrefixExperiment.acceptance line 558
  66. theorem OAI.DirectedFeedback.PrefixExperiment.full_count_expectation line 563
  67. theorem OAI.DirectedFeedback.PrefixExperiment.acceptance_lower_bound line 591
  68. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.Uses line 626
  69. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.splice line 629
  70. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.splicePair line 632
  71. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.splicePair_weight line 638
  72. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_splicePair line 650
  73. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_disjoint line 659
  74. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_disjoint_pattern line 685
  75. abbrev OAI.DirectedFeedback.Coupling.Block line 712
  76. def OAI.DirectedFeedback.Coupling.blockWeight line 714
  77. def OAI.DirectedFeedback.Coupling.block line 722
  78. theorem OAI.DirectedFeedback.Coupling.block_big line 732
  79. theorem OAI.DirectedFeedback.Coupling.block_small line 740
  80. theorem OAI.DirectedFeedback.Coupling.block_inclusion line 748
  81. def OAI.DirectedFeedback.Coupling.flatten line 753
  82. def OAI.DirectedFeedback.Coupling.bigBits line 766
  83. def OAI.DirectedFeedback.Coupling.smallBits line 769
  84. def OAI.DirectedFeedback.Coupling.law line 771
  85. theorem OAI.DirectedFeedback.Coupling.flatten_weight line 774
  86. theorem OAI.DirectedFeedback.Coupling.flatten_expectation line 783
  87. theorem OAI.DirectedFeedback.Coupling.big_expectation line 792
  88. theorem OAI.DirectedFeedback.Coupling.small_expectation line 802
  89. theorem OAI.DirectedFeedback.Coupling.big_probability line 811
  90. theorem OAI.DirectedFeedback.Coupling.small_probability line 818
  91. theorem OAI.DirectedFeedback.Coupling.disjoint_pattern line 825
  92. structure OAI.DirectedFeedback.Games.Game line 857
  93. def OAI.DirectedFeedback.Games.Game.score line 863
  94. def OAI.DirectedFeedback.Games.Game.Sound line 866
  95. def OAI.DirectedFeedback.Games.listChoice line 869