OAI/Computability/DirectedFeedback/Probability/Mixture.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.mixture line 13
  2. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_mixture line 23
  3. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_mixture_le line 40
  4. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.weight_eq_probability_singleton line 59
  5. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.pushforward_comp line 64
  6. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.transport_eq_pushforward line 72
  7. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_pushforward line 80
  8. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.pushforward_mixture line 89
  9. def OAI.DFVSGames.Clean.bernoulli line 108
  10. def OAI.DFVSGames.Clean.maskCount line 114
  11. theorem OAI.DFVSGames.Clean.product_mask line 117
  12. theorem OAI.DFVSGames.Clean.iid_product_moment line 122
  13. theorem OAI.DFVSGames.Clean.bernoulli_mask_moment line 132
  14. def OAI.DFVSGames.Clean.cleanProbability line 149
  15. theorem OAI.DFVSGames.Clean.cleanProbability_nonneg line 153
  16. theorem OAI.DFVSGames.Clean.cleanProbability_le_one line 157
  17. def OAI.DFVSGames.Clean.singletonSlopeLaw line 164
  18. def OAI.DFVSGames.Clean.cleanBit line 168
  19. theorem OAI.DFVSGames.Clean.clean_pushforward line 172
  20. theorem OAI.DFVSGames.Clean.clean_mask_law line 192
  21. theorem OAI.DFVSGames.Clean.clean_mask_moment line 200
  22. theorem OAI.DFVSGames.Clean.cleanProbability_ge_of_card_le line 210
  23. theorem OAI.DFVSGames.Clean.cleanProbability_ge_dimension line 216
  24. theorem OAI.DFVSGames.Clean.mask_rate_antitone line 223
  25. theorem OAI.DFVSGames.Clean.clean_mask_moment_le line 231
  26. theorem OAI.DFVSGames.Clean.clean_mask_moment_le_dimension line 244
  27. theorem OAI.DFVSGames.Clean.mask_rate_le_exp line 253
  28. theorem OAI.DFVSGames.Clean.clean_mask_moment_le_exp line 263
  29. theorem OAI.DFVSGames.Clean.cube_singleton_probability_nonneg line 279
  30. theorem OAI.DFVSGames.Clean.cube_singleton_probability_le_one line 282
  31. theorem OAI.DFVSGames.Clean.cube_mask_rate_le_exp line 290
  32. theorem OAI.DFVSGames.Clean.exists_cube_exponential_lt line 312
  33. theorem OAI.DFVSGames.Clean.exists_cube_mask_rate_lt line 331
  34. abbrev OAI.DFVSGames.Clean.Experiment.Coefficient line 353
  35. abbrev OAI.DFVSGames.Clean.Experiment.Additional line 354
  36. abbrev OAI.DFVSGames.Clean.Experiment.SparseSeed line 355
  37. def OAI.DFVSGames.Clean.Experiment.singletonSet line 357
  38. def OAI.DFVSGames.Clean.Experiment.coefficients line 360
  39. theorem OAI.DFVSGames.Clean.Experiment.zeroSet_eq_cleanMask line 369
  40. theorem OAI.DFVSGames.Clean.Experiment.zeroSet_card line 380
  41. abbrev OAI.DFVSGames.Clean.Experiment.LocalStrategies line 386
  42. def OAI.DFVSGames.Clean.Experiment.success line 389
  43. theorem OAI.DFVSGames.Clean.Experiment.expectation_mono_inline_Experiment line 399
  44. theorem OAI.DFVSGames.Clean.Experiment.expectation_const_inline_Experiment line 405
  45. theorem OAI.DFVSGames.Clean.Experiment.success_le_of_repetition line 409
  46. theorem OAI.DFVSGames.Clean.Experiment.randomized_success_le_of_repetition line 436
  47. def OAI.DFVSGames.Soundness.SubsetIntersection.subsets line 462
  48. def OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean line 465
  49. def OAI.DFVSGames.Soundness.SubsetIntersection.independentMean line 468
  50. def OAI.DFVSGames.Soundness.SubsetIntersection.memberIndicator line 471
  51. def OAI.DFVSGames.Soundness.SubsetIntersection.overlapProbability line 474
  52. theorem OAI.DFVSGames.Soundness.SubsetIntersection.independentMean_eq_double_sum line 477
  53. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_mul_left line 485
  54. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_mul_right line 491
  55. theorem OAI.DFVSGames.Soundness.SubsetIntersection.independentMean_product line 497
  56. theorem OAI.DFVSGames.Soundness.SubsetIntersection.subsets_card line 501
  57. theorem OAI.DFVSGames.Soundness.SubsetIntersection.subsets_nonempty line 504
  58. theorem OAI.DFVSGames.Soundness.SubsetIntersection.subsets_card_ne_zero line 508
  59. theorem OAI.DFVSGames.Soundness.SubsetIntersection.count_containing line 512
  60. theorem OAI.DFVSGames.Soundness.SubsetIntersection.choose_predecessor_ratio line 519
  61. theorem OAI.DFVSGames.Soundness.SubsetIntersection.inclusion_probability line 529
  62. theorem OAI.DFVSGames.Soundness.SubsetIntersection.independent_inclusion_probability line 539
  63. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_congr line 545
  64. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_const line 550
  65. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_finset_sum line 556
  66. theorem OAI.DFVSGames.Soundness.SubsetIntersection.uniformMean_mono line 564
  67. theorem OAI.DFVSGames.Soundness.SubsetIntersection.independentMean_mono line 569
  68. theorem OAI.DFVSGames.Soundness.SubsetIntersection.intersection_card_indicator line 577
  69. theorem OAI.DFVSGames.Soundness.SubsetIntersection.expected_intersection_fixed line 581
  70. theorem OAI.DFVSGames.Soundness.SubsetIntersection.expected_intersection line 588
  71. theorem OAI.DFVSGames.Soundness.SubsetIntersection.nonempty_indicator_le_card line 602
  72. theorem OAI.DFVSGames.Soundness.SubsetIntersection.overlap_probability_le line 608
  73. abbrev OAI.DFVSGames.Soundness.PartnerSampling.ActiveSet line 622
  74. abbrev OAI.DFVSGames.Soundness.PartnerSampling.Partner line 624
  75. theorem OAI.DFVSGames.Soundness.PartnerSampling.activeSet_card line 626
  76. theorem OAI.DFVSGames.Soundness.PartnerSampling.slotTuples_card line 629
  77. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_card line 633
  78. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_nonempty line 639
  79. theorem OAI.DFVSGames.Soundness.PartnerSampling.uniformMean_real_cast line 643
  80. theorem OAI.DFVSGames.Soundness.PartnerSampling.independentMean_real_cast line 649
  81. theorem OAI.DFVSGames.Soundness.PartnerSampling.subset_overlap_probability_le line 655
  82. theorem OAI.DFVSGames.Soundness.PartnerSampling.activeSet_expect line 665
  83. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_expect_activeSet line 670
  84. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_expect_active line 683
  85. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_pair_expect_active line 687
  86. theorem OAI.DFVSGames.Soundness.PartnerSampling.partner_active_overlap_probability_le line 698
  87. def OAI.DFVSGames.Soundness.PartnerSampling.active line 704
  88. def OAI.DFVSGames.Soundness.PartnerSampling.decodeSlot line 707
  89. def OAI.DFVSGames.Soundness.PartnerSampling.slots line 710
  90. def OAI.DFVSGames.Soundness.PartnerSampling.kernel line 713
  91. def OAI.DFVSGames.Soundness.PartnerSampling.activeSubtypeEquiv line 717
  92. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_finrank line 721
  93. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_inf_finrank_le line 729
  94. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_inf_eq_bot_of_no_overlap line 736
  95. def OAI.DFVSGames.Soundness.PartnerSampling.activeOverlap line 749
  96. def OAI.DFVSGames.Soundness.PartnerSampling.kernelCollision line 752
  97. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernelCollision_le_activeOverlap line 757
  98. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_collision_probability_le line 767
  99. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_overlap_weight_pointwise line 781
  100. theorem OAI.DFVSGames.Soundness.PartnerSampling.kernel_overlap_weight_le line 797