OAI/Probability/InvariantIsing/Fields/PriorSiteModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity in the finite ordinary-field variances for an actual fixed spin/leaf prior, uniformly in its spin constraints.

  1. lemma OAI.InvariantIsing.prior_site_pressure_modulus line 13
  2. lemma OAI.InvariantIsing.continuous_prior_site_pressure line 51