OAI/Probability/InvariantIsing/Arrays/TensorCascadeWard.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The countable principal Ward bound for the actual enriched Gibbs law, including the random cascade reference weights.

  1. theorem OAI.InvariantIsing.tensorNamespaced_off_principal_bound line 17