OAI/Probability/EntangledGames/BlockStates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.QuantumSampling.trace_blockDiagonal line 13
  2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_blockDiagonal line 18
  3. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_blockDiagonal line 23
  4. lemma OAI.ThresholdParallelRepetition.QuantumSampling.posSemidef_blockDiagonal line 31
  5. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.blocks line 44
  6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_blockDiagonal line 55
  7. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_eq_zero_iff line 76
  8. def OAI.ThresholdParallelRepetition.QuantumSampling.unitize line 83
  9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_unitize line 86
  10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.unitize_distance line 93
  11. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_difference_unbounded line 108
  12. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_difference_unbounded line 126
  13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.posSemidef_fromBlocks_diag line 148
  14. def OAI.ThresholdParallelRepetition.QuantumSampling.squareState line 161
  15. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_squareState line 164
  16. lemma OAI.ThresholdParallelRepetition.QuantumSampling.squareState_sub line 168
  17. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.sum line 172
  18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_squareState line 183
  19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_squareState line 193
  20. def OAI.ThresholdParallelRepetition.QuantumSampling.weightedBlock line 208
  21. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_weightedBlock line 210
  22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.weightedBlock_sub line 214
  23. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_weightedBlock_sub line 218
  24. lemma OAI.ThresholdParallelRepetition.QuantumSampling.payoff_weightedBlock line 222
  25. lemma OAI.ThresholdParallelRepetition.QuantumSampling.correlated_sampling_value_rect line 229
  26. lemma OAI.ThresholdParallelRepetition.QuantumSampling.avg_payoff_difference_unbounded line 245