OAI/Probability/InvariantIsing/Magnetic/RestrictedFiniteModelDepth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common-depth preservation in the actual normalized finite spectral model.

  1. theorem OAI.InvariantIsing.restricted_cavity_finite_model_depth_test line 15