OAI/Probability/EntangledGames/ExposureErrors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.coord_entropy_nonneg line 12
2. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.list_coord_entropy_sum_le line 18
3. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawA_error_eq line 47
4. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawB_error_eq line 59
5. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.raw_error_bounds line 72
6. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.M line 85
7. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.N line 87
8. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.M_unit line 89
9. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.N_unit line 91
10. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.norm_cost_bounds line 94
11. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.normalized_error_bounds line 119