OAI/Probability/InvariantIsing/Fields/FieldSpinProjectionEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Energy lost by projection in a possibly unbounded external field. The Euclidean estimate is suited to averaging under Gaussian path laws.

  1. lemma OAI.InvariantIsing.fieldEnergy_projection_sq line 14
  2. theorem OAI.InvariantIsing.fieldEnergy_projection_mean_le line 31