OAI/Computability/DirectedFeedback/RankGraph/LastBias.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Construction.big_badness line 99
  2. theorem OAI.DirectedFeedback.Construction.small_badness line 121
  3. theorem OAI.DirectedFeedback.Construction.edge_badness line 142
  4. theorem OAI.DirectedFeedback.Soundness.acceptance_forces_tail line 164
  5. theorem OAI.DirectedFeedback.Soundness.geometric_half_sum line 198
  6. theorem OAI.DirectedFeedback.Soundness.dyadic_layer_cake line 204
  7. theorem OAI.DirectedFeedback.Soundness.dyadic_tails_expectation line 222
  8. theorem OAI.DirectedFeedback.Soundness.dyadic_contradiction line 254
  9. def OAI.DirectedFeedback.Construction.lastBias line 285
  10. theorem OAI.DirectedFeedback.Construction.lastBias_le line 288
  11. theorem OAI.DirectedFeedback.Construction.weighted_soundness line 304
  12. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.expectation_iid_prod line 376
  13. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_sublevel_exp line 382
  14. def OAI.DirectedFeedback.Pivotal.countTrue line 400
  15. theorem OAI.DirectedFeedback.Pivotal.exp_neg_count line 402
  16. theorem OAI.DirectedFeedback.Pivotal.expMoment_count line 406
  17. theorem OAI.DirectedFeedback.Pivotal.expMoment_count_le line 415
  18. theorem OAI.DirectedFeedback.Pivotal.exp_neg_one_le line 430
  19. theorem OAI.DirectedFeedback.Pivotal.bernoulli_lower_tail line 437
  20. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.pushforward_bool line 459
  21. theorem OAI.DirectedFeedback.Pivotal.iid_event_lower_tail line 485
  22. theorem OAI.DirectedFeedback.Coupling.support_inclusion line 503
  23. theorem OAI.DirectedFeedback.Construction.comparison_support_coupling line 528
  24. theorem OAI.DirectedFeedback.Construction.comparison_label_increases line 539
  25. theorem OAI.DirectedFeedback.Construction.subset_eval_probability line 592
  26. theorem OAI.DirectedFeedback.Construction.slot_label_probability line 602
  27. theorem OAI.DirectedFeedback.Construction.fullCount_lower_tail line 626
  28. theorem OAI.DirectedFeedback.Construction.fullStars_probability line 652
  29. theorem OAI.DirectedFeedback.Pivotal.labelOrder_label_probability line 702
  30. def OAI.DirectedFeedback.Construction.labelDeleted line 722
  31. def OAI.DirectedFeedback.Construction.labelFeedback line 726
  32. theorem OAI.DirectedFeedback.Construction.labelFeedback_spec line 730
  33. theorem OAI.DirectedFeedback.Construction.labelFeedback_indicator line 734
  34. theorem OAI.DirectedFeedback.Construction.full_label_cost line 740
  35. theorem OAI.DirectedFeedback.Construction.big_label_cost line 754
  36. theorem OAI.DirectedFeedback.Construction.small_label_cost line 776
  37. theorem OAI.DirectedFeedback.Construction.comparison_label_cost line 792
  38. theorem OAI.DirectedFeedback.Construction.weighted_completeness line 827
  39. structure OAI.DirectedFeedback.Construction.Parameters line 856
  40. theorem OAI.DirectedFeedback.Construction.exists_parameters line 874
  41. instance OAI.DirectedFeedback.Construction.Parameters.(instance at line 920) line 920
  42. instance OAI.DirectedFeedback.Construction.Parameters.(instance at line 921) line 921
  43. theorem OAI.DirectedFeedback.Construction.Parameters.gamma_pos line 923
  44. theorem OAI.DirectedFeedback.Construction.Parameters.gamma_le line 925
  45. theorem OAI.DirectedFeedback.Construction.Parameters.full_error line 929
  46. theorem OAI.DirectedFeedback.Construction.Parameters.product_error line 936
  47. structure OAI.DirectedFeedback.Construction.RankParameters line 951
  48. theorem OAI.DirectedFeedback.Construction.exists_rankParameters line 964