OAI/Probability/InvariantIsing/Cavity/CavityFieldBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform height bounds for the actual fields reconstructed from a finite spectral law. These bounds are independent of the overlap partition.

  1. lemma OAI.InvariantIsing.cavityFieldPrimitive_le line 14
  2. lemma OAI.InvariantIsing.cavityFieldStep_height_le line 25