OAI/Probability/EntangledGames/Basic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThresholdParallelRepetition.Strategy.born_eq_quadratic line 16
2. lemma OAI.ThresholdParallelRepetition.Strategy.born_nonneg line 22
3. lemma OAI.ThresholdParallelRepetition.Strategy.total_effect line 28
4. lemma OAI.ThresholdParallelRepetition.Strategy.born_sum line 39
5. lemma OAI.ThresholdParallelRepetition.Strategy.born_le_one line 50
6. def OAI.ThresholdParallelRepetition.Strategy.deterministic line 62
7. lemma OAI.ThresholdParallelRepetition.successProbability_nonneg line 85
8. lemma OAI.ThresholdParallelRepetition.successProbability_le_one line 96
9. lemma OAI.ThresholdParallelRepetition.entangledValue_nonneg line 113
10. lemma OAI.ThresholdParallelRepetition.successProbability_le_value line 121
11. lemma OAI.ThresholdParallelRepetition.entangledValue_le_one line 126