OAI/Probability/ClassicalON/JointBond.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.amplitudeBondParam line 14
  2. theorem OAI.ClassicalON.amplitudeBondParam_nonneg line 18
  3. theorem OAI.ClassicalON.amplitudeBondParam_monotone line 26
  4. theorem OAI.ClassicalON.continuous_amplitudeBondParam line 38
  5. def OAI.ClassicalON.bondConditionalMean line 42
  6. theorem OAI.ClassicalON.continuous_bondConditionalMean line 47
  7. theorem OAI.ClassicalON.bondConditionalMean_nonneg line 63
  8. theorem OAI.ClassicalON.bondConditionalMean_monotone line 68
  9. def OAI.ClassicalON.jointBondMean line 78
  10. theorem OAI.ClassicalON.jointBond_associated line 83