OAI/Probability/FreeIsing/Ising/CopyFixedPathBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingCopySpectral.inner_rooted_cavityLogVector_eq_of_length_eq line 19
2. theorem OAI.Problem367.IsingCopySpectral.inner_pathValue_eq_rooted_cavityLogVector line 36
3. theorem OAI.Problem367.IsingCopySpectral.inner_forwardOperator_eq_rooted_cavityLogVector line 58
4. theorem OAI.Problem367.IsingCopySpectral.abs_inner_rooted_cavityLogVector_le_norm_pow line 70
5. theorem OAI.Problem367.IsingCopySpectral.exists_rooted_cavityLogVector_correlation_bound line 85
6. theorem OAI.Problem367.IsingCopySpectral.exists_rooted_cavityLogDifference_pair_bound line 101