OAI/Probability/InvariantIsing/Fields/FieldHeightSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar-field supporting inequality on strict finite height vectors. The Hessian criterion follows from the mixed and radial derivative signs.

  1. theorem OAI.InvariantIsing.fieldHeight_support_strict line 15