OAI/Probability/InvariantIsing/Fields/PhysicalFieldPopulationLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity of physical mean pressure under matching limiting finite spectral and field populations. Zero limiting field weights are allowed.

  1. theorem OAI.InvariantIsing.physical_mean_field_populations_tendsto line 13
  2. theorem OAI.InvariantIsing.physical_mean_joint_populations_tendsto line 34