OAI/Probability/ClassicalON/RawBond.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.amplitudeBondPrefactor line 14
2. def OAI.ClassicalON.amplitudeBondWeight line 18
3. theorem OAI.ClassicalON.amplitudeBondPrefactor_pos line 21
4. theorem OAI.ClassicalON.continuous_amplitudeBondPrefactor line 26
5. theorem OAI.ClassicalON.continuous_amplitudeBondWeight line 33
6. theorem OAI.ClassicalON.amplitudeBondWeight_nonneg line 44
7. theorem OAI.ClassicalON.amplitudeBondWeight_sum line 49
8. theorem OAI.ClassicalON.amplitudeDensity_bondConditionalMean line 57
9. theorem OAI.ClassicalON.jointBondMean_raw line 69