OAI/Computability/DirectedFeedback/RankGraph/PrefixBit.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Construction.vertices_takePrefix line 76
  2. def OAI.DirectedFeedback.Construction.prefixBit line 87
  3. theorem OAI.DirectedFeedback.Construction.prefixBit_properties line 92
  4. def OAI.DirectedFeedback.Construction.prefixTransition line 100
  5. theorem OAI.DirectedFeedback.Construction.prefixBit_lift line 106
  6. theorem OAI.DirectedFeedback.Construction.full_membership line 113
  7. def OAI.DirectedFeedback.Construction.favorable line 178
  8. def OAI.DirectedFeedback.Construction.prefixValue line 182
  9. theorem OAI.DirectedFeedback.Construction.favorable_count line 189
  10. theorem OAI.DirectedFeedback.Construction.favorable_probability line 211
  11. theorem OAI.DirectedFeedback.Construction.full_acceptance line 233
  12. def OAI.DirectedFeedback.Ranks.Homogeneous line 264
  13. theorem OAI.DirectedFeedback.Ranks.end_homogeneous line 267
  14. theorem OAI.DirectedFeedback.Ranks.finite_ramsey line 330
  15. def OAI.DirectedFeedback.Ranks.payoff line 373
  16. theorem OAI.DirectedFeedback.Ranks.payoff_left line 376
  17. theorem OAI.DirectedFeedback.Ranks.payoff_right line 381
  18. def OAI.DirectedFeedback.Ranks.probabilitySimplex line 388
  19. theorem OAI.DirectedFeedback.Ranks.single_mem_probabilitySimplex line 391
  20. theorem OAI.DirectedFeedback.Ranks.convex_probabilitySimplex line 395
  21. theorem OAI.DirectedFeedback.Ranks.isCompact_probabilitySimplex line 405
  22. theorem OAI.DirectedFeedback.Ranks.finite_minimax line 423
  23. theorem OAI.DirectedFeedback.Ranks.rational_simplex_approximation line 462
  24. abbrev OAI.DirectedFeedback.Ranks.Triple line 533
  25. abbrev OAI.DirectedFeedback.Ranks.Increasing line 534
  26. theorem OAI.DirectedFeedback.Ranks.triple_nonempty line 536
  27. def OAI.DirectedFeedback.Ranks.toFinite line 542
  28. theorem OAI.DirectedFeedback.Ranks.toFinite_image line 545
  29. abbrev OAI.DirectedFeedback.Ranks.RankTest line 551
  30. def OAI.DirectedFeedback.Ranks.rankPayoff line 553
  31. theorem OAI.DirectedFeedback.Ranks.rankPayoff_abs line 557
  32. theorem OAI.DirectedFeedback.Ranks.bucket_close line 562
  33. theorem OAI.DirectedFeedback.Ranks.rank_spreading line 571
  34. def OAI.DirectedFeedback.Ranks.Spreads line 680
  35. theorem OAI.DirectedFeedback.Ranks.exists_spreading_law line 685
  36. theorem OAI.DirectedFeedback.Ranks.triple_data_processing line 696
  37. def OAI.DirectedFeedback.Ranks.tripleVector line 723
  38. theorem OAI.DirectedFeedback.Ranks.tripleVector_strict line 725
  39. theorem OAI.DirectedFeedback.RankGraph.comparison_expectations line 739
  40. theorem OAI.DirectedFeedback.RankGraph.ordered_disagreement line 752
  41. theorem OAI.DirectedFeedback.RankGraph.compare_marker_mono line 766
  42. theorem OAI.DirectedFeedback.RankGraph.comparison_disagreement line 777
  43. theorem OAI.DirectedFeedback.RankGraph.goodness_probability line 839
  44. theorem OAI.DirectedFeedback.RankGraph.domain_card_bound line 882
  45. theorem OAI.DirectedFeedback.RankGraph.goodness_bound line 896
  46. theorem OAI.DirectedFeedback.RankGraph.sampled_goodness line 908
  47. theorem OAI.DirectedFeedback.Construction.full_badness line 945