OAI/Probability/EntangledGames/TestExtraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold line 14
2. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_nonneg line 16
3. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_le_one line 19
4. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_markov line 23
5. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_mean_bound line 36
6. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.geometric_bound line 46
7. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_power_bound line 55
8. lemma OAI.ThresholdParallelRepetition.RepeatedModel.all_event_step line 83
9. lemma OAI.ThresholdParallelRepetition.RepeatedModel.threshold_power_bound line 107
10. lemma OAI.ThresholdParallelRepetition.RepeatedModel.threshold_mean_bound line 116