OAI/Probability/InvariantIsing/Spectral/SpectralContactTails.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Synchronized field-contact tests include the root and identify every partition-endpoint tail without excluding atoms at those endpoints.

  1. lemma OAI.InvariantIsing.spectralSpin_integral line 16
  2. lemma OAI.InvariantIsing.spectralPair_depthTail_integral line 37
  3. lemma OAI.InvariantIsing.contact_partition_tail_order line 64