OAI/Probability/InvariantIsing/Fields/FieldGaussianProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A separable scalar cavity tilt preserves independence of the Gaussian site coordinates. This identifies the actual vector transition law.

  1. theorem OAI.InvariantIsing.fieldGaussian_product_tilt line 14