FieldAffineShape.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Evenness, monotonicity and the unit spin bound for the actual affine log-cosh recursion. These hypotheses of the mixed-order argument are discharged from the explicit terminal function.

theorem OAI.InvariantIsing.fieldAffineFamily_shape line 16