OAI/Probability/EntangledGames/EffectExposure.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_posSemidef line 16
  2. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_matrix_mono line 21
  3. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_matrix_le line 25
  4. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_posSemidef line 32
  5. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_posSemidef line 39
  6. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_le line 46
  7. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_le line 53
  8. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.le_one line 63
  9. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.coarsen line 67
  10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.POVM.coarsen_sum line 74
  11. def OAI.ThresholdParallelRepetition.QuantumSampling.POVM.average line 81
  12. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.potential_left_lower line 93
  13. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.potential_right_lower line 108
  14. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.potential_left_nonpos line 124
  15. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.potential_right_nonpos line 134
  16. def OAI.ThresholdParallelRepetition.Resolvent.effectIndex line 148
  17. def OAI.ThresholdParallelRepetition.Resolvent.commonMap line 151
  18. lemma OAI.ThresholdParallelRepetition.Resolvent.effectIndex_eq line 155
  19. lemma OAI.ThresholdParallelRepetition.Resolvent.commonMap_gram line 159
  20. lemma OAI.ThresholdParallelRepetition.Resolvent.commonMap_jensen line 164
  21. lemma OAI.ThresholdParallelRepetition.Resolvent.commonMap_error_left line 179
  22. lemma OAI.ThresholdParallelRepetition.Resolvent.commonMap_error_right line 197