OAI/Probability/ClassicalON/FamilyBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClassicalON.SpinSystem.coefficientObservable_norm_le line 15
2. theorem OAI.ClassicalON.SpinSystem.averageComplex_pos_square line 24
3. theorem OAI.ClassicalON.SpinSystem.norm_averageComplex_sum_le line 34
4. def OAI.ClassicalON.SpinSystem.familyPaired line 41
5. def OAI.ClassicalON.SpinSystem.familyRemainder line 46
6. theorem OAI.ClassicalON.SpinSystem.familyObservable_contraction line 66