OAI/Probability/InvariantIsing/Fields/FieldEnergyCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar-field forest as a finite Ising energy-mark forest.

  1. lemma OAI.InvariantIsing.measurable_fieldEnergy_map line 14
  2. lemma OAI.InvariantIsing.fieldEnergy_map_norm_le line 18
  3. def OAI.InvariantIsing.fieldEnergyMarkLaw line 30
  4. lemma OAI.InvariantIsing.fieldEnergyMarkLaw_moments line 33
  5. def OAI.InvariantIsing.fieldEnergyCoordinates line 50
  6. lemma OAI.InvariantIsing.measurable_fieldEnergyCoordinates line 55
  7. theorem OAI.InvariantIsing.fieldEnergyCoordinates_law line 60
  8. lemma OAI.InvariantIsing.fieldEnergyCoordinates_energy line 79
  9. theorem OAI.InvariantIsing.field_vector_spin_exp_integrable line 95