OAI/Probability/EntangledGames/HilbertSchmidt.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThresholdParallelRepetition.QuantumSampling.hsSq line 21
2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_nonneg line 23
3. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_conjTranspose line 26
4. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_eq_trace line 30
5. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_eq_trace' line 40
6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_mul_left line 43
7. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_mul_right line 49
8. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_spectral_mixed line 55
9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_cfc_sub_le line 93
10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_abs_sub_le line 108
11. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_zero line 116
12. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_blocks line 118
13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.fromBlocks_sub line 127
14. lemma OAI.ThresholdParallelRepetition.QuantumSampling.block_diagonal_pos line 134
15. def OAI.ThresholdParallelRepetition.QuantumSampling.dilation line 147
16. lemma OAI.ThresholdParallelRepetition.QuantumSampling.dilation_isHermitian line 151
17. lemma OAI.ThresholdParallelRepetition.QuantumSampling.abs_square line 156
18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.abs_eq_sqrt_square line 170
19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.sqrt_block_diagonal line 175
20. lemma OAI.ThresholdParallelRepetition.QuantumSampling.abs_dilation line 185
21. theorem OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_right_absolute_sub_le line 194