OAI/Probability/InvariantIsing/Arrays/TensorGrowingDepthGG.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full vector GG for growing finite cascades. The only additional condition is the explicit vanishing finite-model rate, attainable by choosing the system sizes along a sufficiently fast subsequence.

  1. theorem OAI.InvariantIsing.tensor_growing_depth_minimizers_spectralGG line 15