OAI/Probability/Ising/TwoSpin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BufferedIsing.tableConstant line 10

   Source documentation

   Walsh coefficients of the log of a positive two-spin table.

   noncomputable def tableConstant (w : Bool → Bool → ℝ) : ℝ :=
   …

2. def OAI.BufferedIsing.tableCoupling line 14
3. def OAI.BufferedIsing.tableFieldLeft line 18
4. def OAI.BufferedIsing.tableFieldRight line 22
5. lemma OAI.BufferedIsing.table_expansion line 26
6. def OAI.BufferedIsing.balancedTable line 36
7. lemma OAI.BufferedIsing.balancedTable_eq line 39
8. def OAI.BufferedIsing.tableExpectation line 45
9. lemma OAI.BufferedIsing.balancedTable_means line 48
10. lemma OAI.BufferedIsing.balancedTable_correlation line 54