OAI/Probability/InvariantIsing/Fields/FieldProductSpinAveraging.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independent endpoint fields followed by their Gibbs spin draws have the product of the averaged one-site spin laws. This identifies the projection-distance average appearing in the terminal-loss estimate.

  1. lemma OAI.InvariantIsing.scalarSpinKernel_atom_integrable line 16
  2. lemma OAI.InvariantIsing.scalarSpinKernel_average_atom line 29
  3. theorem OAI.InvariantIsing.field_product_spin_average line 42