OAI/Probability/EntangledGames/CorrelatedSampling.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.QuantumSampling.norm_eq_sqrt_hsSq line 23
  2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_le_one_norm line 26
  3. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_difference_le line 29
  4. def OAI.ThresholdParallelRepetition.QuantumSampling.winEffect line 48
  5. lemma OAI.ThresholdParallelRepetition.QuantumSampling.winEffect_pos line 50
  6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.winEffect_le_one line 57
  7. def OAI.ThresholdParallelRepetition.QuantumSampling.flat line 69
  8. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_flat line 71
  9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.flat_sub line 74
  10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.flat_form line 76
  11. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_eq_form line 81
  12. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_eq_hsSq line 90
  13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.winSqrt_contraction line 98
  14. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_difference_le line 104
  15. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_ratio_loss line 119
  16. theorem OAI.ThresholdParallelRepetition.QuantumSampling.filter_approximation_value line 140
  17. def OAI.ThresholdParallelRepetition.QuantumSampling.rowBlocks line 182
  18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rowBlocks_mul_transpose line 184
  19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rowBlocks_mul_diagonal line 191
  20. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_rowBlocks line 199
  21. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_transpose line 205
  22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.projectionRows_gram line 209
  23. lemma OAI.ThresholdParallelRepetition.QuantumSampling.projectionRows_contraction line 222
  24. def OAI.ThresholdParallelRepetition.QuantumSampling.binResource line 236
  25. def OAI.ThresholdParallelRepetition.QuantumSampling.bobBinFilter line 238
  26. lemma OAI.ThresholdParallelRepetition.QuantumSampling.bobBinFilter_contraction line 240
  27. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binResource_transpose line 251
  28. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binResource_pos line 253
  29. lemma OAI.ThresholdParallelRepetition.QuantumSampling.bin_output line 261
  30. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_polar_bin line 270
  31. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_roundedAbs_eq_sum line 275
  32. lemma OAI.ThresholdParallelRepetition.QuantumSampling.bin_left_mass line 284
  33. lemma OAI.ThresholdParallelRepetition.QuantumSampling.bin_right_mass line 291
  34. theorem OAI.ThresholdParallelRepetition.QuantumSampling.correlated_sampling_value line 301