OAI/Probability/EntangledGames/SamplingStrategy.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ThresholdParallelRepetition.QuantumSampling.POVM line 19
2. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.default line 27
3. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.pull line 33
4. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.pull_pos line 37
5. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.pull_sum line 40
6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.kronecker_sum_left line 45
7. lemma OAI.ThresholdParallelRepetition.QuantumSampling.kronecker_sum_right line 49
8. def OAI.ThresholdParallelRepetition.QuantumSampling.Copies line 53
9. instance OAI.ThresholdParallelRepetition.QuantumSampling.copiesFintype line 56
10. instance OAI.ThresholdParallelRepetition.QuantumSampling.copiesDecidableEq line 61
11. instance OAI.ThresholdParallelRepetition.QuantumSampling.copiesNonempty line 64
12. def OAI.ThresholdParallelRepetition.QuantumSampling.tensorPower line 70
13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_tensorPower line 74
14. def OAI.ThresholdParallelRepetition.QuantumSampling.firstSuccess line 80
15. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_submatrix line 94
16. lemma OAI.ThresholdParallelRepetition.QuantumSampling.exists_strategy_of_finite line 106
17. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_first_step_ge line 146
18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.firstSuccess_prob_succ line 161
19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_sum_left line 183
20. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_sum_right line 187
21. def OAI.ThresholdParallelRepetition.QuantumSampling.payoff line 197
22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_total line 199
23. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_nonneg line 202
24. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_le_hsSq line 209
25. lemma OAI.ThresholdParallelRepetition.QuantumSampling.firstSuccess_prob_geometric line 219
26. lemma OAI.ThresholdParallelRepetition.QuantumSampling.firstSuccess_payoff_geometric line 252
27. lemma OAI.ThresholdParallelRepetition.QuantumSampling.finite_filter_geometric_value line 268
28. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_sub_left line 297
29. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_sub_right line 301
30. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_gram line 306
31. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_left_gram line 310
32. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_right_gram line 315
33. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_fail line 320
34. lemma OAI.ThresholdParallelRepetition.QuantumSampling.filter_mass_bounds line 327
35. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_fail_le line 345
36. lemma OAI.ThresholdParallelRepetition.QuantumSampling.output_zero_of_fail_full line 353
37. lemma OAI.ThresholdParallelRepetition.QuantumSampling.geometric_contribution_tendsto line 363
38. theorem OAI.ThresholdParallelRepetition.QuantumSampling.finite_filter_value line 372
39. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_smul line 397
40. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_smul line 405
41. theorem OAI.ThresholdParallelRepetition.QuantumSampling.finite_filter_value_unnormalized line 410