OAI/Probability/InvariantIsing/Fields/SpinPriorPerturbationVariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform concentration of the actual finite perturbation for a deterministic spin constraint, with the cascade retained as quenched disorder.

  1. theorem OAI.InvariantIsing.spinPriorPerturbation_variance line 13