OAI/Probability/FreeIsing/Energy/FiniteLeafCovariance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.LeafGibbs.expectation line 13
  2. theorem OAI.Problem367.LeafGibbs.expectation_eq_mean_zero line 16
  3. def OAI.Problem367.LeafGibbs.covariance line 21
  4. def OAI.Problem367.LeafGibbs.energy line 24
  5. lemma OAI.Problem367.LeafGibbs.expectation_add line 28
  6. lemma OAI.Problem367.LeafGibbs.expectation_const_mul line 32
  7. lemma OAI.Problem367.LeafGibbs.expectation_mul_const line 36
  8. lemma OAI.Problem367.LeafGibbs.expectation_const line 40
  9. lemma OAI.Problem367.LeafGibbs.spin_exponential_mean line 47
  10. lemma OAI.Problem367.LeafGibbs.tanh_leaf_affine line 58
  11. theorem OAI.Problem367.LeafGibbs.expectation_mul_leaf_eq line 68
  12. theorem OAI.Problem367.LeafGibbs.expectation_mul_leaf_affine line 98
  13. theorem OAI.Problem367.LeafGibbs.covariance_leaf_eq_mul_parent line 117
  14. lemma OAI.Problem367.LeafGibbs.spin_variance_bounds line 130
  15. theorem OAI.Problem367.LeafGibbs.covariance_parent_leaf line 140
  16. theorem OAI.Problem367.LeafGibbs.covariance_parent_leaf_bounds line 150