OAI/Probability/EntangledGames/Refinement.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.transport line 14
  2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.transport_pullback line 19
  3. structure OAI.ThresholdParallelRepetition.MixedExposure.Refinement line 31
  4. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftFine line 42
  5. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightFine line 44
  6. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftFine_pos line 47
  7. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightFine_pos line 50
  8. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftFine_total line 53
  9. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightFine_total line 60
  10. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftFine_local line 67
  11. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightFine_local line 70
  12. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftPOVM line 73
  13. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightPOVM line 76
  14. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.leftPOVM_local line 81
  15. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.rightPOVM_local line 89
  16. instance OAI.ThresholdParallelRepetition.MixedExposure.Refinement.coherentDecEq line 97
  17. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.P line 101
  18. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.Q line 104
  19. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.P_effect line 109
  20. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.Q_effect line 117
  21. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.transported_prob line 125
  22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_weightedBlock line 143
  23. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.prob_D line 157
  24. def OAI.ThresholdParallelRepetition.MixedExposure.Refinement.score line 182
  25. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.avg_if_massAt line 187
  26. lemma OAI.ThresholdParallelRepetition.MixedExposure.Refinement.payoff_D_eq_score line 204