OAI/Probability/InvariantIsing/Fields/FieldAffineNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every strict affine covariance vector has a common neighborhood where the finite recursion has uniformly positive and bounded variances.

  1. lemma OAI.InvariantIsing.fieldAffine_variance_neighborhood line 14