OAI/Probability/FreeIsing/Estimates/FiniteChain.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteChain.weight line 9
  2. def OAI.Problem367.FiniteChain.endpoint line 13
  3. theorem OAI.Problem367.FiniteChain.weight_zero line 17
  4. theorem OAI.Problem367.FiniteChain.endpoint_zero line 20
  5. theorem OAI.Problem367.FiniteChain.weight_cons line 23
  6. theorem OAI.Problem367.FiniteChain.endpoint_cons line 27
  7. theorem OAI.Problem367.FiniteChain.weight_eq_prod line 31
  8. theorem OAI.Problem367.FiniteChain.endpoint_eq_last line 39
  9. theorem OAI.Problem367.FiniteChain.weight_nonneg line 47
  10. theorem OAI.Problem367.FiniteChain.sum_cons line 55
  11. def OAI.Problem367.FiniteChain.expectation line 61
  12. theorem OAI.Problem367.FiniteChain.expectation_zero line 64
  13. theorem OAI.Problem367.FiniteChain.expectation_succ line 68
  14. theorem OAI.Problem367.FiniteChain.expectation_eigenfunction line 74
  15. theorem OAI.Problem367.FiniteChain.sum_weight line 90