OAI/Computability/BinPacking/Games/RepetitionUpper.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

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