OAI/Computability/DirectedFeedback/RankGraph/CellCount.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Prefix.transition_membership line 16
  2. theorem OAI.DirectedFeedback.Prefix.starred_transition line 40
  3. def OAI.DirectedFeedback.Prefix.cellCount line 70
  4. theorem OAI.DirectedFeedback.Prefix.cellCount_eq line 74
  5. def OAI.DirectedFeedback.Prefix.prefixCell line 79
  6. def OAI.DirectedFeedback.Prefix.splitLast line 83
  7. def OAI.DirectedFeedback.Prefix.stepFunction line 89
  8. theorem OAI.DirectedFeedback.Prefix.stepFunction_mono line 92
  9. theorem OAI.DirectedFeedback.Prefix.stepFunction_lift line 97
  10. theorem OAI.DirectedFeedback.Prefix.step_transition line 101
  11. def OAI.DirectedFeedback.Prefix.conditionedValue line 106
  12. theorem OAI.DirectedFeedback.Prefix.selected_parent line 110
  13. theorem OAI.DirectedFeedback.Prefix.selected_last line 125
  14. theorem OAI.DirectedFeedback.Prefix.full_transition_membership line 137
  15. def OAI.DirectedFeedback.Prefix.orderedCell line 164
  16. theorem OAI.DirectedFeedback.Prefix.block_prefix line 172
  17. theorem OAI.DirectedFeedback.Prefix.ordered_boundary_sdiff line 192
  18. theorem OAI.DirectedFeedback.Prefix.single_label_crossing line 202
  19. structure OAI.DirectedFeedback.SourceProbability.FiniteDistribution line 239
  20. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation line 248
  21. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability line 251
  22. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_nonnegative line 254
  23. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_le_one line 262
  24. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_true line 271
  25. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_false line 275
  26. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_mono line 279
  27. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pushforward line 291
  28. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_pushforward line 303
  29. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.transport line 315
  30. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_transport line 320
  31. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.iid line 326
  32. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_iid_all line 331
  33. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.eq_of_weight_eq line 351
  34. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.table line 361
  35. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_table_eval line 372
  36. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.table_eval_pushforward line 400
  37. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.product line 414
  38. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_product line 423
  39. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_comm line 429
  40. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_congr line 442
  41. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.iid_pushforward line 449
  42. def OAI.DirectedFeedback.SourceProbability.FiniteDistribution.uniform line 469
  43. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.iid_uniform line 478
  44. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_uniform line 485
  45. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_const line 497
  46. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_mono line 501
  47. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_nonneg line 505
  48. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_add line 509
  49. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_mul_left line 513
  50. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_sum line 517
  51. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_pushforward line 522
  52. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_uniform_eq_expect line 531
  53. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.table_pushforward line 535
  54. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.table_uniform line 554
  55. def OAI.DirectedFeedback.Probability.andBit line 566
  56. def OAI.DirectedFeedback.Probability.andCoin line 568
  57. theorem OAI.DirectedFeedback.Probability.andCoin_true line 571
  58. theorem OAI.DirectedFeedback.Probability.andCoin_false line 576
  59. def OAI.DirectedFeedback.Probability.dyadicLaw line 581
  60. theorem OAI.DirectedFeedback.Probability.dyadicLaw_weight line 584
  61. def OAI.DirectedFeedback.Probability.blockAnd line 590
  62. theorem OAI.DirectedFeedback.Probability.blockAnd_expectation line 592
  63. def OAI.DirectedFeedback.Pivotal.coin line 610
  64. def OAI.DirectedFeedback.Pivotal.law line 615
  65. def OAI.DirectedFeedback.Pivotal.relabel line 618
  66. theorem OAI.DirectedFeedback.Pivotal.relabel_apply line 625
  67. theorem OAI.DirectedFeedback.Pivotal.relabel_trans line 629
  68. theorem OAI.DirectedFeedback.Pivotal.law_relabel line 632
  69. def OAI.DirectedFeedback.Pivotal.chainPrefix line 647
  70. theorem OAI.DirectedFeedback.Pivotal.sorted_chainPrefix line 650
  71. def OAI.DirectedFeedback.Pivotal.chainHit line 681
  72. def OAI.DirectedFeedback.Pivotal.chainBudget line 684
  73. theorem OAI.DirectedFeedback.Pivotal.uniform_comp_right line 687
  74. theorem OAI.DirectedFeedback.Pivotal.probability_eq_expectation line 701
  75. theorem OAI.DirectedFeedback.Pivotal.bernoulli_le_chainBudget line 708
  76. def OAI.DirectedFeedback.Pivotal.atom line 749
  77. def OAI.DirectedFeedback.Pivotal.bitValue line 751
  78. def OAI.DirectedFeedback.Pivotal.insertBit line 753
  79. theorem OAI.DirectedFeedback.Pivotal.insertBit_self line 757
  80. theorem OAI.DirectedFeedback.Pivotal.insertBit_other line 761
  81. theorem OAI.DirectedFeedback.Pivotal.sum_split line 765
  82. theorem OAI.DirectedFeedback.Pivotal.prod_except line 771
  83. def OAI.DirectedFeedback.Pivotal.acceptance line 775
  84. def OAI.DirectedFeedback.Pivotal.discreteDerivative line 778
  85. def OAI.DirectedFeedback.Pivotal.totalInfluence line 782
  86. theorem OAI.DirectedFeedback.Pivotal.acceptance_eq_probability line 786
  87. theorem OAI.DirectedFeedback.Pivotal.atom_hasDerivAt line 792
  88. theorem OAI.DirectedFeedback.Pivotal.russo line 798
  89. def OAI.DirectedFeedback.Pivotal.pivotalEvent line 816
  90. def OAI.DirectedFeedback.Pivotal.budget line 820
  91. theorem OAI.DirectedFeedback.Pivotal.discreteDerivative_eq_indicator line 824
  92. theorem OAI.DirectedFeedback.Pivotal.totalInfluence_eq_sum_probability line 836
  93. theorem OAI.DirectedFeedback.Pivotal.influence_le_budget line 846
  94. theorem OAI.DirectedFeedback.Pivotal.influence_nonneg line 852
  95. theorem OAI.DirectedFeedback.Pivotal.acceptance_zero line 858