OAI/Probability/EntangledGames/Rounding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThresholdParallelRepetition.Game.questionLaw line 13
2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rounding_value_rect line 17
3. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rounding_value_modes line 53
4. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.uniform line 99
5. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.uniform_avg line 103
6. lemma OAI.ThresholdParallelRepetition.rounding_loss_small line 111
7. lemma OAI.ThresholdParallelRepetition.MixedExposure.conditional_rounding_bound line 160
8. lemma OAI.ThresholdParallelRepetition.MixedExposure.conditional_rounding_small line 189
9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.coarsen_prob_sum line 215
10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.coarsen_slice line 231
11. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_POVM_total line 242
12. def OAI.ThresholdParallelRepetition.QuantumSampling.outcomeLaw line 246
13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.outcomeLaw_avg line 251