OAI/Probability/InvariantIsing/Cavity/CavityRotationVectorNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual base-model group vectors satisfy the size bound required by logarithmic coefficient replacement.

  1. lemma OAI.InvariantIsing.cavity_rotation_vectors_norm_bound line 14