OAI/Probability/EntangledGames/MeasurementTransport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThresholdParallelRepetition.MeasurementTransport.supportInverse line 21
2. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.supportInverse_isHermitian line 23
3. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.supportInverse_mul_self_mul line 26
4. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.self_mul_supportInverse_mul line 40
5. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.supportInverse_commute line 55
6. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.bounded_mulVec_zero line 72
7. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.bounded_mul_zero line 81
8. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.right_support line 88
9. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.left_support line 96
10. def OAI.ThresholdParallelRepetition.MeasurementTransport.rangeProjection line 104
11. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.rangeProjection_isHermitian line 108
12. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.rangeProjection_sq line 115
13. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.complement_posSemidef line 124
14. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.complement_pullback line 133
15. def OAI.ThresholdParallelRepetition.MeasurementTransport.transportedEffect line 144
16. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.transportedEffect_pos line 149
17. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.transportedEffect_sum line 156
18. lemma OAI.ThresholdParallelRepetition.MeasurementTransport.transportedEffect_pullback line 168
19. theorem OAI.ThresholdParallelRepetition.MeasurementTransport.measurement_transport line 188