OAI/Probability/SKValue/GroundState/LiteralLower.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKValue.shiftedCoefficientSum_le_groundState line 14
2. lemma OAI.SKValueG.finiteMaximum_prod_add line 39
3. lemma OAI.SKValueG.finiteMaximum_prod_curry line 51
4. lemma OAI.SKValueG.spinMaximum_eq_sum_abs line 64
5. def OAI.SKValueG.leafField line 82
6. lemma OAI.SKValueG.linearProcess_leafField line 86
7. lemma OAI.SKValueG.leafField_max line 96
8. lemma OAI.SKValueG.expected_guerra_max line 103
9. theorem OAI.SKValueG.finite_guerra_upper line 137