OAI/Probability/EntangledGames/RelativeEntropy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.negMulLog_subprob line 13
2. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.hellinger_le_entropy line 32
3. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.weighted_negMulLog_le line 47
4. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.avg_entropy_jensen line 73
5. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.avg_entropy_nonneg line 86
6. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.avg_hellinger_le_entropy line 91
7. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.first_density_entropy_le line 103
8. lemma OAI.ThresholdParallelRepetition.ScalarEntropy.second_density_entropy_le line 111
9. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.effectEntropy_nonpos line 124
10. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.spectralLinear_sum line 138
11. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.spectralLinear_single_pos line 146
12. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.spectralLinear_one line 155
13. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.functional_entropy_lower line 159
14. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_smul_left line 190
15. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_smul_right line 194
16. def OAI.ThresholdParallelRepetition.OperatorEntropy.probLeft line 198
17. def OAI.ThresholdParallelRepetition.OperatorEntropy.probRight line 203
18. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_mono_left line 209
19. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_mono_right line 215
20. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_entropy_left_lower line 221
21. lemma OAI.ThresholdParallelRepetition.OperatorEntropy.prob_entropy_right_lower line 228