OAI/Combinatorics/IndependentSets/Repetition/RepetitionUpper.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Soundness.RepetitionUpper.bernoulliAverage line 7
  2. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.bernoulliAverage_scale line 13
  3. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.bernoulliAverage_geometric line 21
  4. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.bernoulliAverage_mono line 33
  5. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.success_le_geometric line 48
  6. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.pow_mono_nonneg line 59
  7. def OAI.IndependentSetsGames.Soundness.RepetitionUpper.zeroProbability line 71
  8. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.zeroProbability_nonneg line 73
  9. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.zeroProbability_le_one line 76
  10. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.zeroProbability_antitone line 84
  11. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.geometric_le_dimension_bound line 103
  12. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.projection_upper_bound line 117
  13. def OAI.IndependentSetsGames.Soundness.RepetitionUpper.decoderThreshold line 128
  14. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.decoderThreshold_pos line 130
  15. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.exists_pos_nat_gt line 139
  16. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.power_mul_growth_le_one line 148
  17. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.exists_power_lt line 164
  18. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.zeroProbability_pos line 181
  19. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.exists_repetition_length line 184
  20. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.soundness_of_bounds line 198
  21. theorem OAI.IndependentSetsGames.Soundness.RepetitionUpper.soundness_from_repetition line 213