OAI/Probability/ClassicalON/BondPin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.pinRestriction line 13
2. def OAI.ClassicalON.bondPinRank line 18
3. def OAI.ClassicalON.bondPinFactor line 21
4. theorem OAI.ClassicalON.bondPinFactor_pos line 25
5. theorem OAI.ClassicalON.bondPinRank_antitone line 28
6. theorem OAI.ClassicalON.bondPinFactor_monotone line 34
7. def OAI.ClassicalON.pinnedBondSubspace line 40
8. theorem OAI.ClassicalON.pinnedBond_rank_add line 44
9. theorem OAI.ClassicalON.pinnedBond_card line 57