OAI/Probability/SKValue/GroundState/RoundingSpin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.boolSign line 12
2. lemma OAI.SKValue.measurable_boolSign line 14
3. lemma OAI.SKValue.spin_boolSign_eq line 17
4. lemma OAI.SKValue.gaussian_rounding_nonzero line 22
5. lemma OAI.SKValue.independent_rounding_nonzero line 32
6. lemma OAI.SKValue.finite_rounding_signed_spin line 44
7. theorem OAI.SKValue.normalized_shifted_sum_le_groundState line 63